Compare commits
13 Commits
main
...
Unreleased
Author | SHA1 | Date |
---|---|---|
Achim D. Brucker | 2341879f06 | |
Achim D. Brucker | 08039609f6 | |
Achim D. Brucker | a8bdb312d0 | |
Achim D. Brucker | 2118c80d65 | |
Achim D. Brucker | bc4ad76a34 | |
Achim D. Brucker | 0700e41a86 | |
Achim D. Brucker | b0262972c3 | |
Achim D. Brucker | e041d45e50 | |
Achim D. Brucker | 15aa0fb133 | |
Achim D. Brucker | 2c8fc958c3 | |
Achim D. Brucker | c5d54e8528 | |
Achim D. Brucker | ec857b177f | |
Achim D. Brucker | e9fefd4602 |
|
@ -5,22 +5,22 @@ pipeline {
|
||||||
stage('Build Docker') {
|
stage('Build Docker') {
|
||||||
steps {
|
steps {
|
||||||
sh 'cp src/patches/thy_output.ML .ci/isabelle4isadof/'
|
sh 'cp src/patches/thy_output.ML .ci/isabelle4isadof/'
|
||||||
sh 'docker build -t logicalhacking:isabelle4dof .ci/isabelle4isadof'
|
sh 'docker build -t logicalhacking:isabelle4dof-2018 .ci/isabelle4isadof'
|
||||||
sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
|
sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
stage('Check Docker') {
|
stage('Check Docker') {
|
||||||
when { changeset "src/patches/*" }
|
when { changeset "src/patches/*" }
|
||||||
steps {
|
steps {
|
||||||
sh 'cp src/patches/thy_output.ML .ci/isabelle4isadof/'
|
sh 'cp patches/thy_output.ML .ci/isabelle4isadof/'
|
||||||
sh 'docker build --no-cache -t logicalhacking:isabelle4dof .ci/isabelle4isadof'
|
sh 'docker build --no-cache -t logicalhacking:isabelle4dof-2018 .ci/isabelle4isadof'
|
||||||
sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
|
sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
stage('Build Isabelle/DOF') {
|
stage('Build Isabelle/DOF') {
|
||||||
steps {
|
steps {
|
||||||
sh 'find -type d -name "output" -exec rm -rf {} \\; || true'
|
sh 'find -type d -name "output" -exec rm -rf {} \\; || true'
|
||||||
sh 'docker run -v $PWD:/DOF logicalhacking:isabelle4dof sh -c "cd /DOF && ./install && isabelle build -D ."'
|
sh 'docker run -v $PWD:/DOF logicalhacking:isabelle4dof-2018 sh -c "cd /DOF && ./install && isabelle build -D ."'
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -24,7 +24,7 @@
|
||||||
#
|
#
|
||||||
# SPDX-License-Identifier: BSD-2-Clause
|
# SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
|
||||||
FROM logicalhacking:isabelle2019
|
FROM logicalhacking:isabelle2018
|
||||||
|
|
||||||
WORKDIR /home/isabelle
|
WORKDIR /home/isabelle
|
||||||
COPY thy_output.ML /home/isabelle/Isabelle/src/Pure/Thy
|
COPY thy_output.ML /home/isabelle/Isabelle/src/Pure/Thy
|
||||||
|
|
8
.config
8
.config
|
@ -1,8 +1,8 @@
|
||||||
DOF_VERSION="Unreleased"
|
DOF_VERSION="Unreleased"
|
||||||
ISABELLE_VERSION="Isabelle2019: June 2019"
|
ISABELLE_VERSION="Isabelle2018: August 2018"
|
||||||
ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2019/"
|
ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2018/"
|
||||||
DOF_URL="https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
DOF_URL="https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
||||||
DOF_ARTIFACT_DIR="releases/Isabelle_DOF/Isabelle_DOF"
|
DOF_ARTIFACT_DIR="releases/Isabelle_DOF/Isabelle_DOF"
|
||||||
DOF_ARTIFACT_HOST="artifacts.logicalhacking.com"
|
DOF_ARTIFACT_HOST="artifacts.logicalhacking.com"
|
||||||
AFP_DATE="afp-2019-06-17"
|
AFP_DATE="afp-2019-06-04"
|
||||||
AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
|
AFP_URL="https://sourceforge.net/projects/afp/files/afp-Isabelle2018/"$AFP_DATE".tar.gz"
|
||||||
|
|
|
@ -8,9 +8,9 @@ development.
|
||||||
|
|
||||||
Isabelle/DOF has two major pre-requisites:
|
Isabelle/DOF has two major pre-requisites:
|
||||||
|
|
||||||
* **Isabelle:** Isabelle/DOF requires [Isabelle 2019](http://isabelle.in.tum.de/website-Isabelle2019/).
|
* **Isabelle:** Isabelle/DOF requires [Isabelle 2018](http://isabelle.in.tum.de/website-Isabelle2018/).
|
||||||
Please download the Isabelle 2019 distribution for your operating
|
Please download the Isabelle 2018 distribution for your operating
|
||||||
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2019/).
|
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2018/).
|
||||||
* **LaTeX:** Isabelle/DOF requires a modern pdfTeX-engine supporting the \expanded{}-primitive. This
|
* **LaTeX:** Isabelle/DOF requires a modern pdfTeX-engine supporting the \expanded{}-primitive. This
|
||||||
is, for example, included in the [TeXLive 2019](https://www.tug.org/texlive/) (or later)
|
is, for example, included in the [TeXLive 2019](https://www.tug.org/texlive/) (or later)
|
||||||
distribution. Please follow the [TeXLive installation instructions](https://www.tug.org/texlive/acquire-netinstall.html)
|
distribution. Please follow the [TeXLive installation instructions](https://www.tug.org/texlive/acquire-netinstall.html)
|
||||||
|
@ -29,7 +29,7 @@ one), the full path to the ``isabelle`` command needs to be passed as
|
||||||
using the ``--isabelle`` command line argument of the ``install`` script:
|
using the ``--isabelle`` command line argument of the ``install`` script:
|
||||||
|
|
||||||
```console
|
```console
|
||||||
foo@bar:~$ ./install --isabelle /usr/local/Isabelle2019/bin/isabelle
|
foo@bar:~$ ./install --isabelle /usr/local/Isabelle2018/bin/isabelle
|
||||||
```
|
```
|
||||||
|
|
||||||
For further command line options of the installer, please use the
|
For further command line options of the installer, please use the
|
||||||
|
|
File diff suppressed because it is too large
Load Diff
|
@ -39,7 +39,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||||
"lemma*" "theorem*" (* -- intended replacement of Isar std commands.*)
|
"lemma*" "theorem*" (* -- intended replacement of Isar std commands.*)
|
||||||
"assert*" ::thy_decl
|
"assert*" ::thy_decl
|
||||||
|
|
||||||
and "print_doc_classes" "print_doc_items" "check_doc_global" :: diag
|
and "print_doc_classes" "print_doc_items" "gen_sty_template" "check_doc_global" :: diag
|
||||||
|
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
@ -627,6 +627,82 @@ val _ =
|
||||||
Outer_Syntax.command \<^command_keyword>\<open>check_doc_global\<close> "check global document consistency"
|
Outer_Syntax.command \<^command_keyword>\<open>check_doc_global\<close> "check global document consistency"
|
||||||
(Parse.opt_bang >> (fn b => Toplevel.keep (check_doc_global b o Toplevel.context_of)));
|
(Parse.opt_bang >> (fn b => Toplevel.keep (check_doc_global b o Toplevel.context_of)));
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
fun write_ontology_latex_sty_template thy =
|
||||||
|
let
|
||||||
|
(*
|
||||||
|
val raw_name = Context.theory_long_name thy
|
||||||
|
|
||||||
|
val curr_thy_name = if String.isPrefix "Draft." raw_name
|
||||||
|
then String.substring(raw_name, 6, (String.size raw_name)-6)
|
||||||
|
else error "Not in ontology definition context"
|
||||||
|
*)
|
||||||
|
val curr_thy_name = Context.theory_name thy
|
||||||
|
val {docobj_tab={tab = x, ...},docclass_tab,...}= get_data_global thy;
|
||||||
|
|
||||||
|
fun toStringLaTeXNewKeyCommand env long_name =
|
||||||
|
"\\expandafter\\newkeycommand\\csname"^" "^"isaDof."^env^"."^long_name^"\\endcsname%\n"
|
||||||
|
|
||||||
|
fun toStringMetaArgs true attr_long_names =
|
||||||
|
enclose "[" "][1]" (commas ("label=,type=%\n" :: attr_long_names))
|
||||||
|
|toStringMetaArgs false attr_long_names =
|
||||||
|
enclose "[" "][1]" (commas attr_long_names)
|
||||||
|
|
||||||
|
fun toStringDocItemBody env =
|
||||||
|
enclose "{%\n\\isamarkupfalse\\isamarkup"
|
||||||
|
"{#1}\\label{\\commandkey{label}}\\isamarkuptrue%\n}\n"
|
||||||
|
env
|
||||||
|
|
||||||
|
fun toStringDocItemCommand env long_name attr_long_names =
|
||||||
|
toStringLaTeXNewKeyCommand env long_name ^
|
||||||
|
toStringMetaArgs true attr_long_names ^
|
||||||
|
toStringDocItemBody env ^"\n"
|
||||||
|
|
||||||
|
fun toStringDocItemLabel long_name attr_long_names =
|
||||||
|
toStringLaTeXNewKeyCommand "Label" long_name ^
|
||||||
|
toStringMetaArgs false attr_long_names ^
|
||||||
|
"{%\n\\autoref{#1}\n}\n"
|
||||||
|
|
||||||
|
fun toStringDocItemRef long_name label attr_long_namesNvalues =
|
||||||
|
"\\isaDof.Label." ^ long_name ^
|
||||||
|
enclose "[" "]" (commas attr_long_namesNvalues) ^
|
||||||
|
enclose "{" "}" label
|
||||||
|
|
||||||
|
fun write_file thy filename content =
|
||||||
|
let
|
||||||
|
val filename = Path.explode filename
|
||||||
|
val master_dir = Resources.master_directory thy
|
||||||
|
val abs_filename = if (Path.is_absolute filename)
|
||||||
|
then filename
|
||||||
|
else Path.append master_dir filename
|
||||||
|
in
|
||||||
|
File.write (abs_filename) content
|
||||||
|
handle (IO.Io{name=name,...})
|
||||||
|
=> warning ("Could not write \""^(name)^"\".")
|
||||||
|
end
|
||||||
|
|
||||||
|
fun write_attr (n, ty, _) = YXML.content_of(Binding.print n)^ "=\n"
|
||||||
|
|
||||||
|
fun write_class (n, {attribute_decl,id,inherits_from,name,params,thy_name,rex,rejectS}) =
|
||||||
|
if curr_thy_name = thy_name then
|
||||||
|
toStringDocItemCommand "section" n (map write_attr attribute_decl) ^
|
||||||
|
toStringDocItemCommand "text" n (map write_attr attribute_decl) ^
|
||||||
|
toStringDocItemLabel n (map write_attr attribute_decl)
|
||||||
|
(* or parameterising with "env" ? ? ?*)
|
||||||
|
else ""
|
||||||
|
val content = String.concat(map write_class (Symtab.dest docclass_tab))
|
||||||
|
(* val _ = writeln content -- for interactive testing only, breaks LaTeX compilation *)
|
||||||
|
in
|
||||||
|
warning("LaTeX Style file generation not supported.")
|
||||||
|
(* write_file thy ("Isa-DOF."^curr_thy_name^".template.sty") content *)
|
||||||
|
end
|
||||||
|
|
||||||
|
|
||||||
|
val _ =
|
||||||
|
Outer_Syntax.command \<^command_keyword>\<open>gen_sty_template\<close> "generate a LaTeX style template"
|
||||||
|
(Parse.opt_bang>>(fn b => Toplevel.keep(write_ontology_latex_sty_template o Toplevel.theory_of)));
|
||||||
|
|
||||||
val (strict_monitor_checking, strict_monitor_checking_setup)
|
val (strict_monitor_checking, strict_monitor_checking_setup)
|
||||||
= Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
|
= Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
|
||||||
|
|
||||||
|
@ -648,7 +724,7 @@ typedecl "thm"
|
||||||
typedecl "file"
|
typedecl "file"
|
||||||
typedecl "thy"
|
typedecl "thy"
|
||||||
|
|
||||||
\<comment> \<open>and others in the future : file, http, thy, ...\<close>
|
\<comment> \<open> and others in the future : file, http, thy, ... \<close>
|
||||||
|
|
||||||
consts ISA_typ :: "string \<Rightarrow> typ" ("@{typ _}")
|
consts ISA_typ :: "string \<Rightarrow> typ" ("@{typ _}")
|
||||||
consts ISA_term :: "string \<Rightarrow> term" ("@{term _}")
|
consts ISA_term :: "string \<Rightarrow> term" ("@{term _}")
|
||||||
|
@ -661,6 +737,8 @@ consts ISA_docitem_attr :: "string \<Rightarrow> string \<Rightarrow> 'a" (
|
||||||
|
|
||||||
\<comment> \<open>Dynamic setup of inner syntax cartouche\<close>
|
\<comment> \<open>Dynamic setup of inner syntax cartouche\<close>
|
||||||
|
|
||||||
|
|
||||||
|
(* PORT TO ISABELLE2018 *)
|
||||||
ML \<open>
|
ML \<open>
|
||||||
(* Author: Frédéric Tuong, Université Paris-Saclay *)
|
(* Author: Frédéric Tuong, Université Paris-Saclay *)
|
||||||
(* Title: HOL/ex/Cartouche_Examples.thy
|
(* Title: HOL/ex/Cartouche_Examples.thy
|
||||||
|
@ -1411,8 +1489,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
|
||||||
in ltx end
|
in ltx end
|
||||||
|
|
||||||
|
|
||||||
fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL)
|
fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) (Symbol.explode (YXML.content_of s)))
|
||||||
(Symbol.explode (YXML.content_of s)))
|
|
||||||
fun ltx_of_markup ctxt s = let
|
fun ltx_of_markup ctxt s = let
|
||||||
val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s
|
val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s
|
||||||
val str_of_term = ltx_of_term ctxt true term
|
val str_of_term = ltx_of_term ctxt true term
|
||||||
|
@ -1425,8 +1502,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
|
||||||
val ctxt = Proof_Context.init_global thy
|
val ctxt = Proof_Context.init_global thy
|
||||||
val actual_args = map (fn ((lhs,_),rhs) => (toLong lhs, ltx_of_markup ctxt rhs))
|
val actual_args = map (fn ((lhs,_),rhs) => (toLong lhs, ltx_of_markup ctxt rhs))
|
||||||
attr_list
|
attr_list
|
||||||
val default_args = map (fn (b,_,t) => (toLong (Long_Name.base_name ( Sign.full_name thy b)),
|
val default_args = map (fn (b,_,t) => (toLong (Long_Name.base_name ( Sign.full_name thy b)), ltx_of_term ctxt true t))
|
||||||
ltx_of_term ctxt true t))
|
|
||||||
(DOF_core.get_attribute_defaults cid_long thy)
|
(DOF_core.get_attribute_defaults cid_long thy)
|
||||||
|
|
||||||
val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a)
|
val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a)
|
||||||
|
@ -1441,7 +1517,7 @@ end
|
||||||
(* the following 2 lines set parser and converter for LaTeX generation of meta-attributes.
|
(* the following 2 lines set parser and converter for LaTeX generation of meta-attributes.
|
||||||
Currently of *all* commands, no distinction between text* and text command.
|
Currently of *all* commands, no distinction between text* and text command.
|
||||||
This code depends on a MODIFIED Isabelle2017 version resulting from applying the files
|
This code depends on a MODIFIED Isabelle2017 version resulting from applying the files
|
||||||
under src/patches.
|
under Isabell_DOF/patches.
|
||||||
*)
|
*)
|
||||||
(* REMARK PORT 2018 : transmission of meta-args to LaTeX crude and untested. Can be found in
|
(* REMARK PORT 2018 : transmission of meta-args to LaTeX crude and untested. Can be found in
|
||||||
present_token. *)
|
present_token. *)
|
||||||
|
@ -1449,13 +1525,14 @@ end
|
||||||
|
|
||||||
end
|
end
|
||||||
\<close>
|
\<close>
|
||||||
ML\<open> (* Setting in thy_output.ML a parser for the syntactic handling of the meta-informations of
|
ML\<open>
|
||||||
text elements - so text*[m<meta-info>]\<open> ... dfgdfg .... \<close> *)
|
|
||||||
|
|
||||||
val _ = Thy_Output.set_meta_args_parser
|
val _ = Thy_Output.set_meta_args_parser
|
||||||
(fn thy => (Scan.optional (Document_Source.improper
|
(fn thy => let val _ = writeln "META_ARGS_PARSING"
|
||||||
|-- ODL_Command_Parser.attributes
|
in (Scan.optional ( ODL_Command_Parser.attributes
|
||||||
>> ODL_LTX_Converter.meta_args_2_string thy) "")); \<close>
|
>> ODL_LTX_Converter.meta_args_2_string thy) "")
|
||||||
|
end);
|
||||||
|
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@ -1545,9 +1622,9 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name =
|
||||||
in () end
|
in () end
|
||||||
else if DOF_core.is_declared_oid_global name thy
|
else if DOF_core.is_declared_oid_global name thy
|
||||||
then (if #strict_checking str
|
then (if #strict_checking str
|
||||||
then warning("declared but undefined document reference: "^name) (* HACK bu 29/6.19 *)
|
then warning("declared but undefined document reference:"^name)
|
||||||
else ())
|
else ())
|
||||||
else error("undefined document reference: "^name)
|
else error("undefined document reference:"^name)
|
||||||
end
|
end
|
||||||
|
|
||||||
val _ = check_and_mark : Proof.context -> string -> {strict_checking: bool} ->
|
val _ = check_and_mark : Proof.context -> string -> {strict_checking: bool} ->
|
||||||
|
@ -1572,13 +1649,13 @@ val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input)
|
||||||
|
|
||||||
fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = y}, src ) =
|
fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = y}, src ) =
|
||||||
let (* val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl) *)
|
let (* val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl) *)
|
||||||
val (str,pos) = Input.source_content src
|
val _ = check_and_mark ctxt cid_decl
|
||||||
val _ = check_and_mark ctxt cid_decl
|
({strict_checking = not x})
|
||||||
({strict_checking = not x}) pos str
|
(Input.pos_of src) (Input.source_content src)
|
||||||
in
|
in
|
||||||
(if y then Latex.enclose_block ("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}]{") "}"
|
(if y then Latex.enclose_block ("\\csname isadof.label[type={"^cid_decl^"}]{") "}\\endcsname"
|
||||||
else Latex.enclose_block ("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}]{") "}")
|
else Latex.enclose_block ("\\csname isadof.ref[type={"^cid_decl^"}]{") "}\\endcsname")
|
||||||
[Latex.text (Input.source_content src)]
|
[Latex.string (Input.source_content src)]
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
||||||
|
@ -1606,7 +1683,7 @@ fun check_and_mark_term ctxt oid =
|
||||||
fun ML_antiquotation_docitem_value (ctxt, toks) =
|
fun ML_antiquotation_docitem_value (ctxt, toks) =
|
||||||
(Scan.lift (Args.cartouche_input)
|
(Scan.lift (Args.cartouche_input)
|
||||||
>> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term)
|
>> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term)
|
||||||
((check_and_mark_term ctxt o fst o Input.source_content) inp)))
|
((check_and_mark_term ctxt o Input.source_content) inp)))
|
||||||
(ctxt, toks)
|
(ctxt, toks)
|
||||||
|
|
||||||
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
|
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
|
||||||
|
|
|
@ -276,36 +276,27 @@ val example_expression : nat rexp =
|
||||||
Times (Star (Plus (Times (r1, r1), r0)), Star (Plus (Times (r0, r0), r1)))
|
Times (Star (Plus (Times (r1, r1), r0)), Star (Plus (Times (r0, r0), r1)))
|
||||||
end;
|
end;
|
||||||
|
|
||||||
|
fun sgn_integer k =
|
||||||
|
(if ((k : IntInf.int) = (0 : IntInf.int)) then (0 : IntInf.int)
|
||||||
|
else (if IntInf.< (k, (0 : IntInf.int)) then (~1 : IntInf.int)
|
||||||
|
else (1 : IntInf.int)));
|
||||||
|
|
||||||
fun divmod_integer k l =
|
fun divmod_integer k l =
|
||||||
(if ((k : IntInf.int) = (0 : IntInf.int))
|
(if ((k : IntInf.int) = (0 : IntInf.int))
|
||||||
then ((0 : IntInf.int), (0 : IntInf.int))
|
then ((0 : IntInf.int), (0 : IntInf.int))
|
||||||
else (if IntInf.< ((0 : IntInf.int), l)
|
else (if ((l : IntInf.int) = (0 : IntInf.int)) then ((0 : IntInf.int), k)
|
||||||
then (if IntInf.< ((0 : IntInf.int), k)
|
else (apsnd o (fn a => fn b => IntInf.* (a, b)) o sgn_integer) l
|
||||||
then IntInf.divMod (IntInf.abs k, IntInf.abs l)
|
(if (((sgn_integer k) : IntInf.int) = (sgn_integer l))
|
||||||
else let
|
then IntInf.divMod (IntInf.abs k, IntInf.abs l)
|
||||||
val (r, s) =
|
else let
|
||||||
IntInf.divMod (IntInf.abs k, IntInf.abs l);
|
val (r, s) =
|
||||||
in
|
IntInf.divMod (IntInf.abs k, IntInf.abs l);
|
||||||
(if ((s : IntInf.int) = (0 : IntInf.int))
|
in
|
||||||
then (IntInf.~ r, (0 : IntInf.int))
|
(if ((s : IntInf.int) = (0 : IntInf.int))
|
||||||
else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
|
then (IntInf.~ r, (0 : IntInf.int))
|
||||||
IntInf.- (l, s)))
|
else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
|
||||||
end)
|
IntInf.- (IntInf.abs l, s)))
|
||||||
else (if ((l : IntInf.int) = (0 : IntInf.int))
|
end)));
|
||||||
then ((0 : IntInf.int), k)
|
|
||||||
else apsnd IntInf.~
|
|
||||||
(if IntInf.< (k, (0 : IntInf.int))
|
|
||||||
then IntInf.divMod (IntInf.abs k, IntInf.abs l)
|
|
||||||
else let
|
|
||||||
val (r, s) =
|
|
||||||
IntInf.divMod (IntInf.abs k, IntInf.abs l);
|
|
||||||
in
|
|
||||||
(if ((s : IntInf.int) = (0 : IntInf.int))
|
|
||||||
then (IntInf.~ r, (0 : IntInf.int))
|
|
||||||
else (IntInf.- (IntInf.~
|
|
||||||
r, (1 : IntInf.int)),
|
|
||||||
IntInf.- (IntInf.~ l, s)))
|
|
||||||
end))));
|
|
||||||
|
|
||||||
fun nat_of_integer k =
|
fun nat_of_integer k =
|
||||||
(if IntInf.<= (k, (0 : IntInf.int)) then Zero_nat
|
(if IntInf.<= (k, (0 : IntInf.int)) then Zero_nat
|
||||||
|
|
|
@ -21,28 +21,19 @@ sig
|
||||||
val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
|
val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
|
||||||
val typewriter: Proof.context -> string -> Latex.text
|
val typewriter: Proof.context -> string -> Latex.text
|
||||||
val verbatim: Proof.context -> string -> Latex.text
|
val verbatim: Proof.context -> string -> Latex.text
|
||||||
val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text
|
val source: Proof.context -> Token.src -> Latex.text
|
||||||
val pretty: Proof.context -> Pretty.T -> Latex.text
|
val pretty: Proof.context -> Pretty.T -> Latex.text
|
||||||
val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text
|
val pretty_source: Proof.context -> Token.src -> Pretty.T -> Latex.text
|
||||||
val pretty_items: Proof.context -> Pretty.T list -> Latex.text
|
val pretty_items: Proof.context -> Pretty.T list -> Latex.text
|
||||||
val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src ->
|
val pretty_items_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
|
||||||
Pretty.T list -> Latex.text
|
|
||||||
val antiquotation_pretty:
|
val antiquotation_pretty:
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
||||||
val antiquotation_pretty_embedded:
|
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
|
||||||
val antiquotation_pretty_source:
|
val antiquotation_pretty_source:
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
||||||
val antiquotation_pretty_source_embedded:
|
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
|
||||||
val antiquotation_raw:
|
val antiquotation_raw:
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
|
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
|
||||||
val antiquotation_raw_embedded:
|
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
|
|
||||||
val antiquotation_verbatim:
|
val antiquotation_verbatim:
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
|
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
|
||||||
val antiquotation_verbatim_embedded:
|
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
|
|
||||||
end;
|
end;
|
||||||
|
|
||||||
structure Thy_Output: THY_OUTPUT =
|
structure Thy_Output: THY_OUTPUT =
|
||||||
|
@ -63,8 +54,8 @@ fun output_comment ctxt (kind, syms) =
|
||||||
Symbol_Pos.cartouche_content syms
|
Symbol_Pos.cartouche_content syms
|
||||||
|> output_symbols
|
|> output_symbols
|
||||||
|> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
|
|> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
|
||||||
| Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
|
| Comment.Latex =>
|
||||||
| Comment.Marker => [])
|
[Latex.symbols (Symbol_Pos.cartouche_content syms)])
|
||||||
and output_comment_document ctxt (comment, syms) =
|
and output_comment_document ctxt (comment, syms) =
|
||||||
(case comment of
|
(case comment of
|
||||||
SOME kind => output_comment ctxt (kind, syms)
|
SOME kind => output_comment ctxt (kind, syms)
|
||||||
|
@ -141,7 +132,6 @@ fun output_token ctxt tok =
|
||||||
in
|
in
|
||||||
(case Token.kind_of tok of
|
(case Token.kind_of tok of
|
||||||
Token.Comment NONE => []
|
Token.Comment NONE => []
|
||||||
| Token.Comment (SOME Comment.Marker) => []
|
|
||||||
| Token.Command => output false "\\isacommand{" "}"
|
| Token.Command => output false "\\isacommand{" "}"
|
||||||
| Token.Keyword =>
|
| Token.Keyword =>
|
||||||
if Symbol.is_ascii_identifier (Token.content_of tok)
|
if Symbol.is_ascii_identifier (Token.content_of tok)
|
||||||
|
@ -163,7 +153,7 @@ fun check_comments ctxt =
|
||||||
val pos = #1 (Symbol_Pos.range syms);
|
val pos = #1 (Symbol_Pos.range syms);
|
||||||
val _ =
|
val _ =
|
||||||
comment |> Option.app (fn kind =>
|
comment |> Option.app (fn kind =>
|
||||||
Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.kind_markups kind)));
|
Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));
|
||||||
val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
|
val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
|
||||||
in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
|
in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
|
||||||
|
|
||||||
|
@ -173,6 +163,15 @@ end;
|
||||||
|
|
||||||
(** present theory source **)
|
(** present theory source **)
|
||||||
|
|
||||||
|
(*NB: arranging white space around command spans is a black art*)
|
||||||
|
|
||||||
|
val is_white = Token.is_space orf Token.is_informal_comment;
|
||||||
|
val is_black = not o is_white;
|
||||||
|
|
||||||
|
val is_white_comment = Token.is_informal_comment;
|
||||||
|
val is_black_comment = Token.is_formal_comment;
|
||||||
|
|
||||||
|
|
||||||
(* presentation tokens *)
|
(* presentation tokens *)
|
||||||
|
|
||||||
datatype token =
|
datatype token =
|
||||||
|
@ -185,8 +184,8 @@ datatype token =
|
||||||
fun basic_token pred (Basic_Token tok) = pred tok
|
fun basic_token pred (Basic_Token tok) = pred tok
|
||||||
| basic_token _ _ = false;
|
| basic_token _ _ = false;
|
||||||
|
|
||||||
val white_token = basic_token Document_Source.is_white;
|
val white_token = basic_token is_white;
|
||||||
val white_comment_token = basic_token Document_Source.is_white_comment;
|
val white_comment_token = basic_token is_white_comment;
|
||||||
val blank_token = basic_token Token.is_blank;
|
val blank_token = basic_token Token.is_blank;
|
||||||
val newline_token = basic_token Token.is_newline;
|
val newline_token = basic_token Token.is_newline;
|
||||||
|
|
||||||
|
@ -200,14 +199,14 @@ fun present_token ctxt tok =
|
||||||
| Markup_Env_Token (cmd, meta_args, source) =>
|
| Markup_Env_Token (cmd, meta_args, source) =>
|
||||||
[Latex.environment_block
|
[Latex.environment_block
|
||||||
("isamarkup" ^ cmd (* ^ meta_args*))
|
("isamarkup" ^ cmd (* ^ meta_args*))
|
||||||
(Latex.string meta_args :: output_document ctxt {markdown = true} source)]
|
(Latex.string meta_args :: output_document ctxt {markdown = true} source)]
|
||||||
| Raw_Token source =>
|
| Raw_Token source =>
|
||||||
Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
|
Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
|
||||||
|
|
||||||
|
|
||||||
(* command spans *)
|
(* command spans *)
|
||||||
|
|
||||||
type command = string * Position.T; (*name, position*)
|
type command = string * Position.T * string list; (*name, position, tags*)
|
||||||
type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
|
type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
|
||||||
|
|
||||||
datatype span = Span of command * (source * source * source * source) * bool;
|
datatype span = Span of command * (source * source * source * source) * bool;
|
||||||
|
@ -231,8 +230,8 @@ fun make_span cmd src =
|
||||||
|
|
||||||
local
|
local
|
||||||
|
|
||||||
fun err_bad_nesting here =
|
fun err_bad_nesting pos =
|
||||||
error ("Bad nesting of commands in presentation" ^ here);
|
error ("Bad nesting of commands in presentation" ^ pos);
|
||||||
|
|
||||||
fun edge which f (x: string option, y) =
|
fun edge which f (x: string option, y) =
|
||||||
if x = y then I
|
if x = y then I
|
||||||
|
@ -243,23 +242,6 @@ val end_tag = edge #1 Latex.end_tag;
|
||||||
fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
|
fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
|
||||||
fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
|
fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
|
||||||
|
|
||||||
fun document_tag cmd_pos state state' tagging_stack =
|
|
||||||
let
|
|
||||||
val ctxt' = Toplevel.presentation_context state';
|
|
||||||
val nesting = Toplevel.level state' - Toplevel.level state;
|
|
||||||
|
|
||||||
val (tagging, taggings) = tagging_stack;
|
|
||||||
val (tag', tagging') = Document_Source.update_tagging ctxt' tagging;
|
|
||||||
|
|
||||||
val tagging_stack' =
|
|
||||||
if nesting = 0 andalso not (Toplevel.is_proof state) then tagging_stack
|
|
||||||
else if nesting >= 0 then (tagging', replicate nesting tagging @ taggings)
|
|
||||||
else
|
|
||||||
(case drop (~ nesting - 1) taggings of
|
|
||||||
tg :: tgs => (tg, tgs)
|
|
||||||
| [] => err_bad_nesting (Position.here cmd_pos));
|
|
||||||
in (tag', tagging_stack') end;
|
|
||||||
|
|
||||||
fun read_tag s =
|
fun read_tag s =
|
||||||
(case space_explode "%" s of
|
(case space_explode "%" s of
|
||||||
["", b] => (SOME b, NONE)
|
["", b] => (SOME b, NONE)
|
||||||
|
@ -275,44 +257,61 @@ fun make_command_tag options keywords =
|
||||||
val document_tags_default = map_filter #1 document_tags;
|
val document_tags_default = map_filter #1 document_tags;
|
||||||
val document_tags_command = map_filter #2 document_tags;
|
val document_tags_command = map_filter #2 document_tags;
|
||||||
in
|
in
|
||||||
fn cmd_name => fn state => fn state' => fn active_tag =>
|
fn {cmd_name, cmd_tags, tag, active_tag} => fn state => fn state' =>
|
||||||
let
|
let
|
||||||
|
val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
|
||||||
|
|
||||||
val keyword_tags =
|
val keyword_tags =
|
||||||
if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
|
if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
|
||||||
else Keyword.command_tags keywords cmd_name;
|
else Keyword.command_tags keywords cmd_name;
|
||||||
val command_tags =
|
val command_tags =
|
||||||
the_list (AList.lookup (op =) document_tags_command cmd_name) @
|
the_list (AList.lookup (op =) document_tags_command cmd_name) @
|
||||||
keyword_tags @ document_tags_default;
|
keyword_tags @ document_tags_default;
|
||||||
|
|
||||||
val active_tag' =
|
val active_tag' =
|
||||||
(case command_tags of
|
if is_some tag' then tag'
|
||||||
default_tag :: _ => SOME default_tag
|
else
|
||||||
| [] =>
|
(case command_tags of
|
||||||
if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
|
default_tag :: _ => SOME default_tag
|
||||||
then active_tag
|
| [] =>
|
||||||
else NONE);
|
if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
|
||||||
in active_tag' end
|
then active_tag
|
||||||
|
else NONE);
|
||||||
|
in {tag' = tag', active_tag' = active_tag'} end
|
||||||
end;
|
end;
|
||||||
|
|
||||||
fun present_span command_tag span state state'
|
fun present_span thy command_tag span state state'
|
||||||
(tagging_stack, active_tag, newline, latex, present_cont) =
|
(tag_stack, active_tag, newline, latex, present_cont) =
|
||||||
let
|
let
|
||||||
val ctxt' = Toplevel.presentation_context state';
|
val ctxt' =
|
||||||
|
Toplevel.presentation_context state'
|
||||||
|
handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN;
|
||||||
val present = fold (fn (tok, (flag, 0)) =>
|
val present = fold (fn (tok, (flag, 0)) =>
|
||||||
fold cons (present_token ctxt' tok)
|
fold cons (present_token ctxt' tok)
|
||||||
#> cons (Latex.string flag)
|
#> cons (Latex.string flag)
|
||||||
| _ => I);
|
| _ => I);
|
||||||
|
|
||||||
val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
|
val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
|
||||||
|
|
||||||
val (tag', tagging_stack') = document_tag cmd_pos state state' tagging_stack;
|
val (tag, tags) = tag_stack;
|
||||||
val active_tag' =
|
val {tag', active_tag'} =
|
||||||
if is_some tag' then Option.map #1 tag'
|
command_tag {cmd_name = cmd_name, cmd_tags = cmd_tags, tag = tag, active_tag = active_tag}
|
||||||
else command_tag cmd_name state state' active_tag;
|
state state';
|
||||||
val edge = (active_tag, active_tag');
|
val edge = (active_tag, active_tag');
|
||||||
|
|
||||||
|
val nesting = Toplevel.level state' - Toplevel.level state;
|
||||||
|
|
||||||
val newline' =
|
val newline' =
|
||||||
if is_none active_tag' then span_newline else newline;
|
if is_none active_tag' then span_newline else newline;
|
||||||
|
|
||||||
|
val tag_stack' =
|
||||||
|
if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
|
||||||
|
else if nesting >= 0 then (tag', replicate nesting tag @ tags)
|
||||||
|
else
|
||||||
|
(case drop (~ nesting - 1) tags of
|
||||||
|
tg :: tgs => (tg, tgs)
|
||||||
|
| [] => err_bad_nesting (Position.here cmd_pos));
|
||||||
|
|
||||||
val latex' =
|
val latex' =
|
||||||
latex
|
latex
|
||||||
|> end_tag edge
|
|> end_tag edge
|
||||||
|
@ -324,7 +323,7 @@ fun present_span command_tag span state state'
|
||||||
val present_cont' =
|
val present_cont' =
|
||||||
if newline then (present (#3 srcs), present (#4 srcs))
|
if newline then (present (#3 srcs), present (#4 srcs))
|
||||||
else (I, present (#3 srcs) #> present (#4 srcs));
|
else (I, present (#3 srcs) #> present (#4 srcs));
|
||||||
in (tagging_stack', active_tag', newline', latex', present_cont') end;
|
in (tag_stack', active_tag', newline', latex', present_cont') end;
|
||||||
|
|
||||||
fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
|
fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
|
||||||
if not (null tags) then err_bad_nesting " at end of theory"
|
if not (null tags) then err_bad_nesting " at end of theory"
|
||||||
|
@ -344,6 +343,14 @@ local
|
||||||
val markup_true = "\\isamarkuptrue%\n";
|
val markup_true = "\\isamarkuptrue%\n";
|
||||||
val markup_false = "\\isamarkupfalse%\n";
|
val markup_false = "\\isamarkupfalse%\n";
|
||||||
|
|
||||||
|
val space_proper =
|
||||||
|
Scan.one Token.is_blank -- Scan.many is_white_comment -- Scan.one is_black;
|
||||||
|
|
||||||
|
val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore);
|
||||||
|
val improper = Scan.many is_improper;
|
||||||
|
val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
|
||||||
|
val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
|
||||||
|
|
||||||
val opt_newline = Scan.option (Scan.one Token.is_newline);
|
val opt_newline = Scan.option (Scan.one Token.is_newline);
|
||||||
|
|
||||||
val ignore =
|
val ignore =
|
||||||
|
@ -353,16 +360,19 @@ val ignore =
|
||||||
(if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
|
(if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
|
||||||
>> pair (d - 1));
|
>> pair (d - 1));
|
||||||
|
|
||||||
|
val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
|
||||||
|
|
||||||
val locale =
|
val locale =
|
||||||
Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |--
|
Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
|
||||||
Parse.!!!
|
Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
|
||||||
(Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")")));
|
|
||||||
|
|
||||||
(*
|
(*
|
||||||
val meta_args_parser_hook = Synchronized.var "meta args parser hook"
|
val meta_args_parser_hook = Synchronized.var "meta args parser hook"
|
||||||
((fn thy => fn s => ("",s)): theory -> string parser);
|
((fn thy => fn s => ("",s)): theory -> string parser);
|
||||||
*)
|
*)
|
||||||
val meta_args_parser_hook = Unsynchronized.ref ((fn _ => fn s => ("",s)): theory -> string parser);
|
val meta_args_parser_hook = Unsynchronized.ref
|
||||||
|
((fn thy => fn s => ("",s)): theory -> string parser);
|
||||||
|
|
||||||
|
|
||||||
in
|
in
|
||||||
|
|
||||||
|
@ -370,6 +380,7 @@ type segment = {span: Command_Span.span, command: Toplevel.transition, state: To
|
||||||
|
|
||||||
fun present_thy options thy (segments: segment list) =
|
fun present_thy options thy (segments: segment list) =
|
||||||
let
|
let
|
||||||
|
|
||||||
val keywords = Thy_Header.get_keywords thy;
|
val keywords = Thy_Header.get_keywords thy;
|
||||||
|
|
||||||
|
|
||||||
|
@ -379,32 +390,30 @@ fun present_thy options thy (segments: segment list) =
|
||||||
>> (fn d => (NONE, (Ignore_Token, ("", d))));
|
>> (fn d => (NONE, (Ignore_Token, ("", d))));
|
||||||
|
|
||||||
fun markup pred mk flag = Scan.peek (fn d =>
|
fun markup pred mk flag = Scan.peek (fn d =>
|
||||||
Document_Source.improper
|
improper |--
|
||||||
|-- Parse.position (Scan.one (fn tok => Token.is_command tok andalso
|
Parse.position (Scan.one (fn tok =>
|
||||||
pred keywords (Token.content_of tok)))
|
Token.is_command tok andalso pred keywords (Token.content_of tok))) --
|
||||||
-- (Document_Source.annotation |--
|
Scan.repeat tag --
|
||||||
(Parse.!!!!
|
(improper |--
|
||||||
( ( (!meta_args_parser_hook thy))
|
(Parse.!!!!
|
||||||
-- ( (Document_Source.improper -- locale -- Document_Source.improper)
|
( (!meta_args_parser_hook thy)
|
||||||
|-- Parse.document_source )
|
-- ( (improper -- locale -- improper)
|
||||||
--| Document_Source.improper_end)
|
|-- (Parse.document_source))
|
||||||
)
|
--| improper_end)))
|
||||||
|
>> (fn (((tok, pos'), tags), (meta_args, source)) =>
|
||||||
)
|
let val name = Token.content_of tok
|
||||||
>> (fn ((tok, pos'), (meta_args, source)) =>
|
in (SOME (name, pos', tags), (mk (name, meta_args, source), (flag, d))) end));
|
||||||
let val name = Token.content_of tok
|
|
||||||
in (SOME (name, pos'), (mk (name, meta_args , source), (flag, d))) end));
|
|
||||||
|
|
||||||
val command = Scan.peek (fn d =>
|
val command = Scan.peek (fn d =>
|
||||||
Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
|
Scan.optional (Scan.one Token.is_command_modifier ::: improper) [] --
|
||||||
Scan.one Token.is_command --| Document_Source.annotation
|
Scan.one Token.is_command -- Scan.repeat tag
|
||||||
>> (fn (cmd_mod, cmd) =>
|
>> (fn ((cmd_mod, cmd), tags) =>
|
||||||
map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
|
map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
|
||||||
[(SOME (Token.content_of cmd, Token.pos_of cmd),
|
[(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
|
||||||
(Basic_Token cmd, (markup_false, d)))]));
|
(Basic_Token cmd, (markup_false, d)))]));
|
||||||
|
|
||||||
val cmt = Scan.peek (fn d =>
|
val cmt = Scan.peek (fn d =>
|
||||||
Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
|
Scan.one is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
|
||||||
|
|
||||||
val other = Scan.peek (fn d =>
|
val other = Scan.peek (fn d =>
|
||||||
Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
|
Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
|
||||||
|
@ -459,25 +468,28 @@ fun present_thy options thy (segments: segment list) =
|
||||||
val command_tag = make_command_tag options keywords;
|
val command_tag = make_command_tag options keywords;
|
||||||
|
|
||||||
fun present_command tr span st st' =
|
fun present_command tr span st st' =
|
||||||
Toplevel.setmp_thread_position tr (present_span command_tag span st st');
|
Toplevel.setmp_thread_position tr (present_span thy command_tag span st st');
|
||||||
|
|
||||||
fun present _ [] = I
|
fun present _ [] = I
|
||||||
| present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
|
| present st ((span, (tr, st')) :: rest) = present_command tr span st st'
|
||||||
|
#> present st' rest;
|
||||||
|
|
||||||
in
|
in
|
||||||
if length command_results = length spans then
|
if length command_results = length spans then
|
||||||
(([], []), NONE, true, [], (I, I))
|
((NONE, []), NONE, true, [], (I, I))
|
||||||
|> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
|
|> present Toplevel.toplevel (spans ~~ command_results)
|
||||||
|> present_trailer
|
|> present_trailer
|
||||||
|> rev
|
|> rev
|
||||||
else error "Messed-up outer syntax for presentation"
|
else error "Messed-up outer syntax for presentation"
|
||||||
end;
|
end;
|
||||||
|
|
||||||
fun set_meta_args_parser f =
|
(*
|
||||||
let
|
fun set_meta_args_parser f = let val _ = writeln "Meta-args parser set to new value"
|
||||||
val _ = writeln "Meta-args parser set to new value"
|
in (Unsynchronized.assign meta_args_parser_hook f) end
|
||||||
in
|
*)
|
||||||
(meta_args_parser_hook := f)
|
fun set_meta_args_parser f = let val _ = writeln "Meta-args parser set to new value"
|
||||||
end
|
in ( meta_args_parser_hook := f) end
|
||||||
|
|
||||||
|
|
||||||
end;
|
end;
|
||||||
|
|
||||||
|
@ -516,19 +528,9 @@ fun verbatim ctxt =
|
||||||
then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
|
then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
|
||||||
else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
|
else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
|
||||||
|
|
||||||
fun token_source ctxt {embedded} tok =
|
fun source ctxt =
|
||||||
if Token.is_kind Token.Cartouche tok andalso embedded andalso
|
|
||||||
not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche)
|
|
||||||
then Token.content_of tok
|
|
||||||
else Token.unparse tok;
|
|
||||||
|
|
||||||
fun is_source ctxt =
|
|
||||||
Config.get ctxt Document_Antiquotation.thy_output_source orelse
|
|
||||||
Config.get ctxt Document_Antiquotation.thy_output_source_cartouche;
|
|
||||||
|
|
||||||
fun source ctxt embedded =
|
|
||||||
Token.args_of_src
|
Token.args_of_src
|
||||||
#> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
|
#> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt)
|
||||||
#> space_implode " "
|
#> space_implode " "
|
||||||
#> output_source ctxt
|
#> output_source ctxt
|
||||||
#> isabelle ctxt;
|
#> isabelle ctxt;
|
||||||
|
@ -536,53 +538,33 @@ fun source ctxt embedded =
|
||||||
fun pretty ctxt =
|
fun pretty ctxt =
|
||||||
Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
|
Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
|
||||||
|
|
||||||
fun pretty_source ctxt embedded src prt =
|
fun pretty_source ctxt src prt =
|
||||||
if is_source ctxt then source ctxt embedded src else pretty ctxt prt;
|
if Config.get ctxt Document_Antiquotation.thy_output_source
|
||||||
|
then source ctxt src else pretty ctxt prt;
|
||||||
|
|
||||||
fun pretty_items ctxt =
|
fun pretty_items ctxt =
|
||||||
map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
|
map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
|
||||||
|
|
||||||
fun pretty_items_source ctxt embedded src prts =
|
fun pretty_items_source ctxt src prts =
|
||||||
if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts;
|
if Config.get ctxt Document_Antiquotation.thy_output_source
|
||||||
|
then source ctxt src else pretty_items ctxt prts;
|
||||||
|
|
||||||
|
|
||||||
(* antiquotation variants *)
|
(* antiquotation variants *)
|
||||||
|
|
||||||
local
|
fun antiquotation_pretty name scan f =
|
||||||
|
Document_Antiquotation.setup name scan
|
||||||
|
(fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
|
||||||
|
|
||||||
fun gen_setup name embedded =
|
fun antiquotation_pretty_source name scan f =
|
||||||
if embedded
|
Document_Antiquotation.setup name scan
|
||||||
then Document_Antiquotation.setup_embedded name
|
(fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
|
||||||
else Document_Antiquotation.setup name;
|
|
||||||
|
|
||||||
fun gen_antiquotation_pretty name embedded scan f =
|
fun antiquotation_raw name scan f =
|
||||||
gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
|
Document_Antiquotation.setup name scan
|
||||||
|
(fn {context = ctxt, argument = x, ...} => f ctxt x);
|
||||||
|
|
||||||
fun gen_antiquotation_pretty_source name embedded scan f =
|
fun antiquotation_verbatim name scan f =
|
||||||
gen_setup name embedded scan
|
antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt);
|
||||||
(fn {context = ctxt, source = src, argument = x} =>
|
|
||||||
pretty_source ctxt {embedded = embedded} src (f ctxt x));
|
|
||||||
|
|
||||||
fun gen_antiquotation_raw name embedded scan f =
|
|
||||||
gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
|
|
||||||
|
|
||||||
fun gen_antiquotation_verbatim name embedded scan f =
|
|
||||||
gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
|
|
||||||
|
|
||||||
in
|
|
||||||
|
|
||||||
fun antiquotation_pretty name = gen_antiquotation_pretty name false;
|
|
||||||
fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
|
|
||||||
|
|
||||||
fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
|
|
||||||
fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
|
|
||||||
|
|
||||||
fun antiquotation_raw name = gen_antiquotation_raw name false;
|
|
||||||
fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
|
|
||||||
|
|
||||||
fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
|
|
||||||
fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
|
|
||||||
|
|
||||||
end;
|
|
||||||
|
|
||||||
end;
|
end;
|
||||||
|
|
|
@ -20,28 +20,19 @@ sig
|
||||||
val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
|
val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
|
||||||
val typewriter: Proof.context -> string -> Latex.text
|
val typewriter: Proof.context -> string -> Latex.text
|
||||||
val verbatim: Proof.context -> string -> Latex.text
|
val verbatim: Proof.context -> string -> Latex.text
|
||||||
val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text
|
val source: Proof.context -> Token.src -> Latex.text
|
||||||
val pretty: Proof.context -> Pretty.T -> Latex.text
|
val pretty: Proof.context -> Pretty.T -> Latex.text
|
||||||
val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text
|
val pretty_source: Proof.context -> Token.src -> Pretty.T -> Latex.text
|
||||||
val pretty_items: Proof.context -> Pretty.T list -> Latex.text
|
val pretty_items: Proof.context -> Pretty.T list -> Latex.text
|
||||||
val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src ->
|
val pretty_items_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
|
||||||
Pretty.T list -> Latex.text
|
|
||||||
val antiquotation_pretty:
|
val antiquotation_pretty:
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
||||||
val antiquotation_pretty_embedded:
|
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
|
||||||
val antiquotation_pretty_source:
|
val antiquotation_pretty_source:
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
||||||
val antiquotation_pretty_source_embedded:
|
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
|
|
||||||
val antiquotation_raw:
|
val antiquotation_raw:
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
|
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
|
||||||
val antiquotation_raw_embedded:
|
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
|
|
||||||
val antiquotation_verbatim:
|
val antiquotation_verbatim:
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
|
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
|
||||||
val antiquotation_verbatim_embedded:
|
|
||||||
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
|
|
||||||
end;
|
end;
|
||||||
|
|
||||||
structure Thy_Output: THY_OUTPUT =
|
structure Thy_Output: THY_OUTPUT =
|
||||||
|
@ -62,8 +53,8 @@ fun output_comment ctxt (kind, syms) =
|
||||||
Symbol_Pos.cartouche_content syms
|
Symbol_Pos.cartouche_content syms
|
||||||
|> output_symbols
|
|> output_symbols
|
||||||
|> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
|
|> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
|
||||||
| Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
|
| Comment.Latex =>
|
||||||
| Comment.Marker => [])
|
[Latex.symbols (Symbol_Pos.cartouche_content syms)])
|
||||||
and output_comment_document ctxt (comment, syms) =
|
and output_comment_document ctxt (comment, syms) =
|
||||||
(case comment of
|
(case comment of
|
||||||
SOME kind => output_comment ctxt (kind, syms)
|
SOME kind => output_comment ctxt (kind, syms)
|
||||||
|
@ -140,7 +131,6 @@ fun output_token ctxt tok =
|
||||||
in
|
in
|
||||||
(case Token.kind_of tok of
|
(case Token.kind_of tok of
|
||||||
Token.Comment NONE => []
|
Token.Comment NONE => []
|
||||||
| Token.Comment (SOME Comment.Marker) => []
|
|
||||||
| Token.Command => output false "\\isacommand{" "}"
|
| Token.Command => output false "\\isacommand{" "}"
|
||||||
| Token.Keyword =>
|
| Token.Keyword =>
|
||||||
if Symbol.is_ascii_identifier (Token.content_of tok)
|
if Symbol.is_ascii_identifier (Token.content_of tok)
|
||||||
|
@ -162,7 +152,7 @@ fun check_comments ctxt =
|
||||||
val pos = #1 (Symbol_Pos.range syms);
|
val pos = #1 (Symbol_Pos.range syms);
|
||||||
val _ =
|
val _ =
|
||||||
comment |> Option.app (fn kind =>
|
comment |> Option.app (fn kind =>
|
||||||
Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups kind)));
|
Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));
|
||||||
val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
|
val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
|
||||||
in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
|
in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
|
||||||
|
|
||||||
|
@ -172,6 +162,15 @@ end;
|
||||||
|
|
||||||
(** present theory source **)
|
(** present theory source **)
|
||||||
|
|
||||||
|
(*NB: arranging white space around command spans is a black art*)
|
||||||
|
|
||||||
|
val is_white = Token.is_space orf Token.is_informal_comment;
|
||||||
|
val is_black = not o is_white;
|
||||||
|
|
||||||
|
val is_white_comment = Token.is_informal_comment;
|
||||||
|
val is_black_comment = Token.is_formal_comment;
|
||||||
|
|
||||||
|
|
||||||
(* presentation tokens *)
|
(* presentation tokens *)
|
||||||
|
|
||||||
datatype token =
|
datatype token =
|
||||||
|
@ -184,8 +183,8 @@ datatype token =
|
||||||
fun basic_token pred (Basic_Token tok) = pred tok
|
fun basic_token pred (Basic_Token tok) = pred tok
|
||||||
| basic_token _ _ = false;
|
| basic_token _ _ = false;
|
||||||
|
|
||||||
val white_token = basic_token Document_Source.is_white;
|
val white_token = basic_token is_white;
|
||||||
val white_comment_token = basic_token Document_Source.is_white_comment;
|
val white_comment_token = basic_token is_white_comment;
|
||||||
val blank_token = basic_token Token.is_blank;
|
val blank_token = basic_token Token.is_blank;
|
||||||
val newline_token = basic_token Token.is_newline;
|
val newline_token = basic_token Token.is_newline;
|
||||||
|
|
||||||
|
@ -204,7 +203,7 @@ fun present_token ctxt tok =
|
||||||
|
|
||||||
(* command spans *)
|
(* command spans *)
|
||||||
|
|
||||||
type command = string * Position.T; (*name, position*)
|
type command = string * Position.T * string list; (*name, position, tags*)
|
||||||
type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
|
type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
|
||||||
|
|
||||||
datatype span = Span of command * (source * source * source * source) * bool;
|
datatype span = Span of command * (source * source * source * source) * bool;
|
||||||
|
@ -228,8 +227,8 @@ fun make_span cmd src =
|
||||||
|
|
||||||
local
|
local
|
||||||
|
|
||||||
fun err_bad_nesting here =
|
fun err_bad_nesting pos =
|
||||||
error ("Bad nesting of commands in presentation" ^ here);
|
error ("Bad nesting of commands in presentation" ^ pos);
|
||||||
|
|
||||||
fun edge which f (x: string option, y) =
|
fun edge which f (x: string option, y) =
|
||||||
if x = y then I
|
if x = y then I
|
||||||
|
@ -240,23 +239,6 @@ val end_tag = edge #1 Latex.end_tag;
|
||||||
fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
|
fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
|
||||||
fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
|
fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
|
||||||
|
|
||||||
fun document_tag cmd_pos state state' tagging_stack =
|
|
||||||
let
|
|
||||||
val ctxt' = Toplevel.presentation_context state';
|
|
||||||
val nesting = Toplevel.level state' - Toplevel.level state;
|
|
||||||
|
|
||||||
val (tagging, taggings) = tagging_stack;
|
|
||||||
val (tag', tagging') = Document_Source.update_tagging ctxt' tagging;
|
|
||||||
|
|
||||||
val tagging_stack' =
|
|
||||||
if nesting = 0 andalso not (Toplevel.is_proof state) then tagging_stack
|
|
||||||
else if nesting >= 0 then (tagging', replicate nesting tagging @ taggings)
|
|
||||||
else
|
|
||||||
(case drop (~ nesting - 1) taggings of
|
|
||||||
tg :: tgs => (tg, tgs)
|
|
||||||
| [] => err_bad_nesting (Position.here cmd_pos));
|
|
||||||
in (tag', tagging_stack') end;
|
|
||||||
|
|
||||||
fun read_tag s =
|
fun read_tag s =
|
||||||
(case space_explode "%" s of
|
(case space_explode "%" s of
|
||||||
["", b] => (SOME b, NONE)
|
["", b] => (SOME b, NONE)
|
||||||
|
@ -272,44 +254,61 @@ fun make_command_tag options keywords =
|
||||||
val document_tags_default = map_filter #1 document_tags;
|
val document_tags_default = map_filter #1 document_tags;
|
||||||
val document_tags_command = map_filter #2 document_tags;
|
val document_tags_command = map_filter #2 document_tags;
|
||||||
in
|
in
|
||||||
fn cmd_name => fn state => fn state' => fn active_tag =>
|
fn {cmd_name, cmd_tags, tag, active_tag} => fn state => fn state' =>
|
||||||
let
|
let
|
||||||
|
val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
|
||||||
|
|
||||||
val keyword_tags =
|
val keyword_tags =
|
||||||
if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
|
if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
|
||||||
else Keyword.command_tags keywords cmd_name;
|
else Keyword.command_tags keywords cmd_name;
|
||||||
val command_tags =
|
val command_tags =
|
||||||
the_list (AList.lookup (op =) document_tags_command cmd_name) @
|
the_list (AList.lookup (op =) document_tags_command cmd_name) @
|
||||||
keyword_tags @ document_tags_default;
|
keyword_tags @ document_tags_default;
|
||||||
|
|
||||||
val active_tag' =
|
val active_tag' =
|
||||||
(case command_tags of
|
if is_some tag' then tag'
|
||||||
default_tag :: _ => SOME default_tag
|
else
|
||||||
| [] =>
|
(case command_tags of
|
||||||
if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
|
default_tag :: _ => SOME default_tag
|
||||||
then active_tag
|
| [] =>
|
||||||
else NONE);
|
if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
|
||||||
in active_tag' end
|
then active_tag
|
||||||
|
else NONE);
|
||||||
|
in {tag' = tag', active_tag' = active_tag'} end
|
||||||
end;
|
end;
|
||||||
|
|
||||||
fun present_span command_tag span state state'
|
fun present_span thy command_tag span state state'
|
||||||
(tagging_stack, active_tag, newline, latex, present_cont) =
|
(tag_stack, active_tag, newline, latex, present_cont) =
|
||||||
let
|
let
|
||||||
val ctxt' = Toplevel.presentation_context state';
|
val ctxt' =
|
||||||
|
Toplevel.presentation_context state'
|
||||||
|
handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN;
|
||||||
val present = fold (fn (tok, (flag, 0)) =>
|
val present = fold (fn (tok, (flag, 0)) =>
|
||||||
fold cons (present_token ctxt' tok)
|
fold cons (present_token ctxt' tok)
|
||||||
#> cons (Latex.string flag)
|
#> cons (Latex.string flag)
|
||||||
| _ => I);
|
| _ => I);
|
||||||
|
|
||||||
val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
|
val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
|
||||||
|
|
||||||
val (tag', tagging_stack') = document_tag cmd_pos state state' tagging_stack;
|
val (tag, tags) = tag_stack;
|
||||||
val active_tag' =
|
val {tag', active_tag'} =
|
||||||
if is_some tag' then Option.map #1 tag'
|
command_tag {cmd_name = cmd_name, cmd_tags = cmd_tags, tag = tag, active_tag = active_tag}
|
||||||
else command_tag cmd_name state state' active_tag;
|
state state';
|
||||||
val edge = (active_tag, active_tag');
|
val edge = (active_tag, active_tag');
|
||||||
|
|
||||||
|
val nesting = Toplevel.level state' - Toplevel.level state;
|
||||||
|
|
||||||
val newline' =
|
val newline' =
|
||||||
if is_none active_tag' then span_newline else newline;
|
if is_none active_tag' then span_newline else newline;
|
||||||
|
|
||||||
|
val tag_stack' =
|
||||||
|
if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
|
||||||
|
else if nesting >= 0 then (tag', replicate nesting tag @ tags)
|
||||||
|
else
|
||||||
|
(case drop (~ nesting - 1) tags of
|
||||||
|
tg :: tgs => (tg, tgs)
|
||||||
|
| [] => err_bad_nesting (Position.here cmd_pos));
|
||||||
|
|
||||||
val latex' =
|
val latex' =
|
||||||
latex
|
latex
|
||||||
|> end_tag edge
|
|> end_tag edge
|
||||||
|
@ -321,7 +320,7 @@ fun present_span command_tag span state state'
|
||||||
val present_cont' =
|
val present_cont' =
|
||||||
if newline then (present (#3 srcs), present (#4 srcs))
|
if newline then (present (#3 srcs), present (#4 srcs))
|
||||||
else (I, present (#3 srcs) #> present (#4 srcs));
|
else (I, present (#3 srcs) #> present (#4 srcs));
|
||||||
in (tagging_stack', active_tag', newline', latex', present_cont') end;
|
in (tag_stack', active_tag', newline', latex', present_cont') end;
|
||||||
|
|
||||||
fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
|
fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
|
||||||
if not (null tags) then err_bad_nesting " at end of theory"
|
if not (null tags) then err_bad_nesting " at end of theory"
|
||||||
|
@ -341,6 +340,14 @@ local
|
||||||
val markup_true = "\\isamarkuptrue%\n";
|
val markup_true = "\\isamarkuptrue%\n";
|
||||||
val markup_false = "\\isamarkupfalse%\n";
|
val markup_false = "\\isamarkupfalse%\n";
|
||||||
|
|
||||||
|
val space_proper =
|
||||||
|
Scan.one Token.is_blank -- Scan.many is_white_comment -- Scan.one is_black;
|
||||||
|
|
||||||
|
val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore);
|
||||||
|
val improper = Scan.many is_improper;
|
||||||
|
val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
|
||||||
|
val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
|
||||||
|
|
||||||
val opt_newline = Scan.option (Scan.one Token.is_newline);
|
val opt_newline = Scan.option (Scan.one Token.is_newline);
|
||||||
|
|
||||||
val ignore =
|
val ignore =
|
||||||
|
@ -350,10 +357,11 @@ val ignore =
|
||||||
(if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
|
(if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
|
||||||
>> pair (d - 1));
|
>> pair (d - 1));
|
||||||
|
|
||||||
|
val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
|
||||||
|
|
||||||
val locale =
|
val locale =
|
||||||
Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |--
|
Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
|
||||||
Parse.!!!
|
Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
|
||||||
(Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")")));
|
|
||||||
|
|
||||||
in
|
in
|
||||||
|
|
||||||
|
@ -370,26 +378,25 @@ fun present_thy options thy (segments: segment list) =
|
||||||
>> (fn d => (NONE, (Ignore_Token, ("", d))));
|
>> (fn d => (NONE, (Ignore_Token, ("", d))));
|
||||||
|
|
||||||
fun markup pred mk flag = Scan.peek (fn d =>
|
fun markup pred mk flag = Scan.peek (fn d =>
|
||||||
Document_Source.improper |--
|
improper |--
|
||||||
Parse.position (Scan.one (fn tok =>
|
Parse.position (Scan.one (fn tok =>
|
||||||
Token.is_command tok andalso pred keywords (Token.content_of tok))) --
|
Token.is_command tok andalso pred keywords (Token.content_of tok))) --
|
||||||
(Document_Source.annotation |--
|
Scan.repeat tag --
|
||||||
Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
|
Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
|
||||||
Parse.document_source --| Document_Source.improper_end))
|
>> (fn (((tok, pos'), tags), source) =>
|
||||||
>> (fn ((tok, pos'), source) =>
|
let val name = Token.content_of tok
|
||||||
let val name = Token.content_of tok
|
in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
|
||||||
in (SOME (name, pos'), (mk (name, source), (flag, d))) end));
|
|
||||||
|
|
||||||
val command = Scan.peek (fn d =>
|
val command = Scan.peek (fn d =>
|
||||||
Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
|
Scan.optional (Scan.one Token.is_command_modifier ::: improper) [] --
|
||||||
Scan.one Token.is_command --| Document_Source.annotation
|
Scan.one Token.is_command -- Scan.repeat tag
|
||||||
>> (fn (cmd_mod, cmd) =>
|
>> (fn ((cmd_mod, cmd), tags) =>
|
||||||
map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
|
map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
|
||||||
[(SOME (Token.content_of cmd, Token.pos_of cmd),
|
[(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
|
||||||
(Basic_Token cmd, (markup_false, d)))]));
|
(Basic_Token cmd, (markup_false, d)))]));
|
||||||
|
|
||||||
val cmt = Scan.peek (fn d =>
|
val cmt = Scan.peek (fn d =>
|
||||||
Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
|
Scan.one is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
|
||||||
|
|
||||||
val other = Scan.peek (fn d =>
|
val other = Scan.peek (fn d =>
|
||||||
Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
|
Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
|
||||||
|
@ -444,14 +451,14 @@ fun present_thy options thy (segments: segment list) =
|
||||||
val command_tag = make_command_tag options keywords;
|
val command_tag = make_command_tag options keywords;
|
||||||
|
|
||||||
fun present_command tr span st st' =
|
fun present_command tr span st st' =
|
||||||
Toplevel.setmp_thread_position tr (present_span command_tag span st st');
|
Toplevel.setmp_thread_position tr (present_span thy command_tag span st st');
|
||||||
|
|
||||||
fun present _ [] = I
|
fun present _ [] = I
|
||||||
| present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
|
| present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
|
||||||
in
|
in
|
||||||
if length command_results = length spans then
|
if length command_results = length spans then
|
||||||
(([], []), NONE, true, [], (I, I))
|
((NONE, []), NONE, true, [], (I, I))
|
||||||
|> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
|
|> present Toplevel.toplevel (spans ~~ command_results)
|
||||||
|> present_trailer
|
|> present_trailer
|
||||||
|> rev
|
|> rev
|
||||||
else error "Messed-up outer syntax for presentation"
|
else error "Messed-up outer syntax for presentation"
|
||||||
|
@ -494,19 +501,9 @@ fun verbatim ctxt =
|
||||||
then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
|
then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
|
||||||
else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
|
else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
|
||||||
|
|
||||||
fun token_source ctxt {embedded} tok =
|
fun source ctxt =
|
||||||
if Token.is_kind Token.Cartouche tok andalso embedded andalso
|
|
||||||
not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche)
|
|
||||||
then Token.content_of tok
|
|
||||||
else Token.unparse tok;
|
|
||||||
|
|
||||||
fun is_source ctxt =
|
|
||||||
Config.get ctxt Document_Antiquotation.thy_output_source orelse
|
|
||||||
Config.get ctxt Document_Antiquotation.thy_output_source_cartouche;
|
|
||||||
|
|
||||||
fun source ctxt embedded =
|
|
||||||
Token.args_of_src
|
Token.args_of_src
|
||||||
#> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
|
#> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt)
|
||||||
#> space_implode " "
|
#> space_implode " "
|
||||||
#> output_source ctxt
|
#> output_source ctxt
|
||||||
#> isabelle ctxt;
|
#> isabelle ctxt;
|
||||||
|
@ -514,53 +511,33 @@ fun source ctxt embedded =
|
||||||
fun pretty ctxt =
|
fun pretty ctxt =
|
||||||
Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
|
Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
|
||||||
|
|
||||||
fun pretty_source ctxt embedded src prt =
|
fun pretty_source ctxt src prt =
|
||||||
if is_source ctxt then source ctxt embedded src else pretty ctxt prt;
|
if Config.get ctxt Document_Antiquotation.thy_output_source
|
||||||
|
then source ctxt src else pretty ctxt prt;
|
||||||
|
|
||||||
fun pretty_items ctxt =
|
fun pretty_items ctxt =
|
||||||
map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
|
map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
|
||||||
|
|
||||||
fun pretty_items_source ctxt embedded src prts =
|
fun pretty_items_source ctxt src prts =
|
||||||
if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts;
|
if Config.get ctxt Document_Antiquotation.thy_output_source
|
||||||
|
then source ctxt src else pretty_items ctxt prts;
|
||||||
|
|
||||||
|
|
||||||
(* antiquotation variants *)
|
(* antiquotation variants *)
|
||||||
|
|
||||||
local
|
fun antiquotation_pretty name scan f =
|
||||||
|
Document_Antiquotation.setup name scan
|
||||||
|
(fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
|
||||||
|
|
||||||
fun gen_setup name embedded =
|
fun antiquotation_pretty_source name scan f =
|
||||||
if embedded
|
Document_Antiquotation.setup name scan
|
||||||
then Document_Antiquotation.setup_embedded name
|
(fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
|
||||||
else Document_Antiquotation.setup name;
|
|
||||||
|
|
||||||
fun gen_antiquotation_pretty name embedded scan f =
|
fun antiquotation_raw name scan f =
|
||||||
gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
|
Document_Antiquotation.setup name scan
|
||||||
|
(fn {context = ctxt, argument = x, ...} => f ctxt x);
|
||||||
|
|
||||||
fun gen_antiquotation_pretty_source name embedded scan f =
|
fun antiquotation_verbatim name scan f =
|
||||||
gen_setup name embedded scan
|
antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt);
|
||||||
(fn {context = ctxt, source = src, argument = x} =>
|
|
||||||
pretty_source ctxt {embedded = embedded} src (f ctxt x));
|
|
||||||
|
|
||||||
fun gen_antiquotation_raw name embedded scan f =
|
|
||||||
gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
|
|
||||||
|
|
||||||
fun gen_antiquotation_verbatim name embedded scan f =
|
|
||||||
gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
|
|
||||||
|
|
||||||
in
|
|
||||||
|
|
||||||
fun antiquotation_pretty name = gen_antiquotation_pretty name false;
|
|
||||||
fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
|
|
||||||
|
|
||||||
fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
|
|
||||||
fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
|
|
||||||
|
|
||||||
fun antiquotation_raw name = gen_antiquotation_raw name false;
|
|
||||||
fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
|
|
||||||
|
|
||||||
fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
|
|
||||||
fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
|
|
||||||
|
|
||||||
end;
|
|
||||||
|
|
||||||
end;
|
end;
|
Loading…
Reference in New Issue