author | wenzelm |
Fri, 20 Sep 2024 15:35:16 +0200 (4 months ago) | |
changeset 80911 | 8ad5e6df050b |
parent 80909 | 6ddbfad8ca20 |
child 80912 | b2eaa342aae5 |
permissions | -rw-r--r-- |
45670 | 1 |
(* Title: Pure/PIDE/markup.ML |
23623 | 2 |
Author: Makarius |
3 |
||
56743 | 4 |
Quasi-abstract markup elements. |
23623 | 5 |
*) |
6 |
||
7 |
signature MARKUP = |
|
8 |
sig |
|
28017 | 9 |
type T = string * Properties.T |
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
10 |
val empty: T |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
11 |
val is_empty: T -> bool |
38229 | 12 |
val properties: Properties.T -> T -> T |
68997 | 13 |
val nameN: string val name: string -> T -> T |
78463
c956b43749f0
clarified signature: systematic use of Properties.make_string;
wenzelm
parents:
78279
diff
changeset
|
14 |
val name_proper: string -> Properties.T |
68997 | 15 |
val xnameN: string val xname: string -> T -> T |
78463
c956b43749f0
clarified signature: systematic use of Properties.make_string;
wenzelm
parents:
78279
diff
changeset
|
16 |
val kindN: string val kind: string -> T -> T |
c956b43749f0
clarified signature: systematic use of Properties.make_string;
wenzelm
parents:
78279
diff
changeset
|
17 |
val kind_proper: string -> Properties.T |
60744 | 18 |
val serialN: string |
19 |
val serial_properties: int -> Properties.T |
|
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
20 |
val instanceN: string |
69889
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
21 |
val meta_titleN: string val meta_title: T |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
22 |
val meta_creatorN: string val meta_creator: T |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
23 |
val meta_contributorN: string val meta_contributor: T |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
24 |
val meta_dateN: string val meta_date: T |
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69916
diff
changeset
|
25 |
val meta_licenseN: string val meta_license: T |
69889
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
26 |
val meta_descriptionN: string val meta_description: T |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
27 |
val languageN: string |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55613
diff
changeset
|
28 |
val symbolsN: string |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
29 |
val delimitedN: string |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
30 |
val is_delimited: Properties.T -> bool |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
31 |
val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
32 |
val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T |
62231
25f4a9cd8b68
tuned markup, e.g. relevant for Rendering.tooltip;
wenzelm
parents:
61864
diff
changeset
|
33 |
val language_Isar: bool -> T |
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55750
diff
changeset
|
34 |
val language_method: T |
56033 | 35 |
val language_attribute: T |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
36 |
val language_sort: bool -> T |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
37 |
val language_type: bool -> T |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
38 |
val language_term: bool -> T |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
39 |
val language_prop: bool -> T |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
40 |
val language_ML: bool -> T |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
41 |
val language_SML: bool -> T |
61600
1ca11ddfcc70
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
wenzelm
parents:
61598
diff
changeset
|
42 |
val language_document: bool -> T |
69887 | 43 |
val language_document_marker: T |
55653
528de9a20054
more markup -- complete symbols within antiquotation, notably with broken arguments;
wenzelm
parents:
55615
diff
changeset
|
44 |
val language_antiquotation: T |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
45 |
val language_text: bool -> T |
62520 | 46 |
val language_verbatim: bool -> T |
67429 | 47 |
val language_latex: bool -> T |
55613 | 48 |
val language_rail: T |
72841 | 49 |
val language_path: bool -> T |
72843 | 50 |
val language_url: bool -> T |
62772 | 51 |
val language_mixfix: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
52 |
val bindingN: string val binding: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
53 |
val entityN: string val entity: string -> string -> T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
54 |
val defN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
55 |
val refN: string |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
56 |
val completionN: string val completion: T |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55837
diff
changeset
|
57 |
val no_completionN: string val no_completion: T |
69557 | 58 |
val updateN: string val update: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
59 |
val lineN: string |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58855
diff
changeset
|
60 |
val end_lineN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
61 |
val offsetN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
62 |
val end_offsetN: string |
78021 | 63 |
val labelN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
64 |
val fileN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
65 |
val idN: string |
74182 | 66 |
val positionN: string val position: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
67 |
val position_properties: string list |
72708 | 68 |
val position_property: Properties.entry -> bool |
74182 | 69 |
val def_name: string -> string |
80911
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
70 |
val notation_mixfixN: string |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
71 |
val notation_infixN: string |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
72 |
val notation_binderN: string |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
73 |
val notations: string list |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
74 |
val notationN: string val notation: {kind: string, name: string} -> T |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
75 |
val notation0: T |
62806 | 76 |
val expressionN: string val expression: string -> T |
80909 | 77 |
val expression0: T |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
78 |
val citationN: string val citation: string -> T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
79 |
val pathN: string val path: string -> T |
70016 | 80 |
val export_pathN: string val export_path: string -> T |
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
81 |
val urlN: string val url: string -> T |
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61614
diff
changeset
|
82 |
val docN: string val doc: string -> T |
72763 | 83 |
val toolN: string val tool: string -> T |
62788 | 84 |
val markupN: string |
85 |
val consistentN: string |
|
62789 | 86 |
val unbreakableN: string |
62786 | 87 |
val block_properties: string list |
62788 | 88 |
val indentN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
89 |
val widthN: string |
61864 | 90 |
val blockN: string val block: bool -> int -> T |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
91 |
val breakN: string val break: int -> int -> T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
92 |
val fbreakN: string val fbreak: T |
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51228
diff
changeset
|
93 |
val itemN: string val item: T |
56548 | 94 |
val wordsN: string val words: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
95 |
val hiddenN: string val hidden: T |
68298
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68101
diff
changeset
|
96 |
val deleteN: string val delete: T |
74671 | 97 |
val load_commandN: string |
71912 | 98 |
val bash_functionN: string |
77028
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
76957
diff
changeset
|
99 |
val bibtex_entryN: string |
71912 | 100 |
val scala_functionN: string |
56465 | 101 |
val system_optionN: string |
67219 | 102 |
val sessionN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
103 |
val theoryN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
104 |
val classN: string |
74112 | 105 |
val localeN: string |
74261
d28a51dd9da6
export other entities, e.g. relevant for formal document output;
wenzelm
parents:
74182
diff
changeset
|
106 |
val bundleN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
107 |
val type_nameN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
108 |
val constantN: string |
74112 | 109 |
val axiomN: string |
110 |
val factN: string |
|
111 |
val oracleN: string |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
112 |
val fixedN: string val fixed: string -> T |
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53055
diff
changeset
|
113 |
val caseN: string val case_: string -> T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
114 |
val dynamic_factN: string val dynamic_fact: string -> T |
63337 | 115 |
val literal_factN: string val literal_fact: string -> T |
74112 | 116 |
val attributeN: string |
117 |
val methodN: string |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57975
diff
changeset
|
118 |
val method_modifierN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
119 |
val tfreeN: string val tfree: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
120 |
val tvarN: string val tvar: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
121 |
val freeN: string val free: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
122 |
val skolemN: string val skolem: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
123 |
val boundN: string val bound: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
124 |
val varN: string val var: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
125 |
val numeralN: string val numeral: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
126 |
val literalN: string val literal: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
127 |
val delimiterN: string val delimiter: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
128 |
val inner_stringN: string val inner_string: T |
55033 | 129 |
val inner_cartoucheN: string val inner_cartouche: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
130 |
val token_rangeN: string val token_range: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
131 |
val sortingN: string val sorting: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
132 |
val typingN: string val typing: T |
63347 | 133 |
val class_parameterN: string val class_parameter: T |
55505 | 134 |
val ML_keyword1N: string val ML_keyword1: T |
135 |
val ML_keyword2N: string val ML_keyword2: T |
|
136 |
val ML_keyword3N: string val ML_keyword3: T |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
137 |
val ML_delimiterN: string val ML_delimiter: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
138 |
val ML_tvarN: string val ML_tvar: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
139 |
val ML_numeralN: string val ML_numeral: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
140 |
val ML_charN: string val ML_char: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
141 |
val ML_stringN: string val ML_string: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
142 |
val ML_commentN: string val ML_comment: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
143 |
val ML_defN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
144 |
val ML_openN: string |
55837 | 145 |
val ML_structureN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
146 |
val ML_typingN: string val ML_typing: T |
60744 | 147 |
val ML_breakpointN: string val ML_breakpoint: int -> T |
55526 | 148 |
val antiquotedN: string val antiquoted: T |
149 |
val antiquoteN: string val antiquote: T |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69345
diff
changeset
|
150 |
val file_typeN: string |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69345
diff
changeset
|
151 |
val antiquotationN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
152 |
val ML_antiquotationN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
153 |
val document_antiquotationN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
154 |
val document_antiquotation_optionN: string |
76514
2615cf68f6f4
ML support for the Prism.js syntax highlighter -- via Isabelle/Scala;
wenzelm
parents:
76394
diff
changeset
|
155 |
val prismjs_languageN: string |
69965
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69962
diff
changeset
|
156 |
val raw_textN: string val raw_text: T |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69962
diff
changeset
|
157 |
val plain_textN: string val plain_text: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
158 |
val paragraphN: string val paragraph: T |
50545
00bdc48c5f71
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
wenzelm
parents:
50543
diff
changeset
|
159 |
val text_foldN: string val text_fold: T |
70229 | 160 |
val document_markerN: string val document_marker: T |
70135
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70016
diff
changeset
|
161 |
val document_tagN: string val document_tag: string -> T |
73780
466fae6bf22e
compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents:
73419
diff
changeset
|
162 |
val document_latexN: string val document_latex: T |
74784
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74673
diff
changeset
|
163 |
val latex_outputN: string val latex_output: T |
74790 | 164 |
val latex_macro0N: string val latex_macro0: string -> T |
165 |
val latex_macroN: string val latex_macro: string -> T |
|
166 |
val latex_environmentN: string val latex_environment: string -> T |
|
74823 | 167 |
val latex_headingN: string val latex_heading: string -> T |
168 |
val latex_bodyN: string val latex_body: string -> T |
|
76957
deb7dffb3340
avoid confusion of markup element vs. property names;
wenzelm
parents:
76956
diff
changeset
|
169 |
val latex_citeN: string val latex_cite: {kind: string, citations: string} -> T |
74786 | 170 |
val latex_index_itemN: string val latex_index_item: T |
171 |
val latex_index_entryN: string val latex_index_entry: string -> T |
|
74826
0e4d8aa61ad7
more symbolic latex_output via XML (using YXML within text);
wenzelm
parents:
74823
diff
changeset
|
172 |
val latex_delimN: string val latex_delim: string -> T |
0e4d8aa61ad7
more symbolic latex_output via XML (using YXML within text);
wenzelm
parents:
74823
diff
changeset
|
173 |
val latex_tagN: string val latex_tag: string -> T |
74836
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
74826
diff
changeset
|
174 |
val optional_argumentN: string val optional_argument: string -> T -> T |
61449 | 175 |
val markdown_paragraphN: string val markdown_paragraph: T |
67323
d02208cefbdb
PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
wenzelm
parents:
67322
diff
changeset
|
176 |
val markdown_itemN: string val markdown_item: T |
67336 | 177 |
val markdown_bulletN: string val markdown_bullet: int -> T |
61449 | 178 |
val markdown_listN: string val markdown_list: string -> T |
67336 | 179 |
val itemizeN: string |
180 |
val enumerateN: string |
|
181 |
val descriptionN: string |
|
59795 | 182 |
val inputN: string val input: bool -> Properties.T -> T |
59935 | 183 |
val command_keywordN: string val command_keyword: T |
78279
dab089b25eb6
more markup for command_span: this allows to reconstruct Thy_Element structure without knowing the outer syntax;
wenzelm
parents:
78021
diff
changeset
|
184 |
val command_spanN: string val command_span: {name: string, kind: string} -> T |
66066 | 185 |
val commandN: string val command_properties: T -> T |
186 |
val keywordN: string val keyword_properties: T -> T |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
187 |
val stringN: string val string: T |
59081 | 188 |
val alt_stringN: string val alt_string: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
189 |
val verbatimN: string val verbatim: T |
55033 | 190 |
val cartoucheN: string val cartouche: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
191 |
val commentN: string val comment: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
192 |
val keyword1N: string val keyword1: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
193 |
val keyword2N: string val keyword2: T |
55763 | 194 |
val keyword3N: string val keyword3: T |
55919
2eb8c13339a5
more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
wenzelm
parents:
55914
diff
changeset
|
195 |
val quasi_keywordN: string val quasi_keyword: T |
56202 | 196 |
val improperN: string val improper: T |
197 |
val operatorN: string val operator: T |
|
69320 | 198 |
val comment1N: string val comment1: T |
199 |
val comment2N: string val comment2: T |
|
200 |
val comment3N: string val comment3: T |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
201 |
val elapsedN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
202 |
val cpuN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
203 |
val gcN: string |
51606
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51570
diff
changeset
|
204 |
val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T |
51228 | 205 |
val parse_command_timing_properties: |
206 |
Properties.T -> ({file: string, offset: int, name: string} * Time.time) option |
|
51606
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51570
diff
changeset
|
207 |
val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T |
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
208 |
val command_indentN: string val command_indent: int -> T |
50543 | 209 |
val goalN: string val goal: T |
50537
08ce81aeeacc
more subgoal markup information, which is potentially useful to manage proof state output;
wenzelm
parents:
50503
diff
changeset
|
210 |
val subgoalN: string val subgoal: string -> T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
211 |
val taskN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
212 |
val forkedN: string val forked: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
213 |
val joinedN: string val joined: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
214 |
val runningN: string val running: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
215 |
val finishedN: string val finished: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
216 |
val failedN: string val failed: T |
68871
f5c76072db55
more explicit status for "canceled" command within theory node;
wenzelm
parents:
68822
diff
changeset
|
217 |
val canceledN: string val canceled: T |
68323 | 218 |
val initializedN: string val initialized: T |
68884
9b97d0b20d95
clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents:
68871
diff
changeset
|
219 |
val finalizedN: string val finalized: T |
70780
034742453594
more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents:
70665
diff
changeset
|
220 |
val consolidatingN: string val consolidating: T |
66379
6392766f3c25
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents:
66066
diff
changeset
|
221 |
val consolidatedN: string val consolidated: T |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50845
diff
changeset
|
222 |
val exec_idN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
223 |
val initN: string |
61209 | 224 |
val statusN: string val status: T |
225 |
val resultN: string val result: T |
|
226 |
val writelnN: string val writeln: T |
|
227 |
val stateN: string val state: T |
|
228 |
val informationN: string val information: T |
|
229 |
val tracingN: string val tracing: T |
|
230 |
val warningN: string val warning: T |
|
231 |
val legacyN: string val legacy: T |
|
232 |
val errorN: string val error: T |
|
233 |
val systemN: string val system: T |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
234 |
val protocolN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
235 |
val reportN: string val report: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
236 |
val no_reportN: string val no_report: T |
64677
8dc24130e8fe
more uniform treatment of "bad" like other messages (with serial number);
wenzelm
parents:
63806
diff
changeset
|
237 |
val badN: string val bad: unit -> T |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
238 |
val intensifyN: string val intensify: T |
73835 | 239 |
val countN: string |
240 |
val ML_profiling_entryN: string |
|
241 |
val ML_profiling_entry: {name: string, count: int} -> T |
|
242 |
val ML_profilingN: string |
|
243 |
val ML_profiling: string -> T |
|
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50683
diff
changeset
|
244 |
val browserN: string |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
245 |
val graphviewN: string |
69650 | 246 |
val theory_exportsN: string |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
247 |
val sendbackN: string |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
248 |
val paddingN: string |
50842 | 249 |
val padding_line: Properties.entry |
52697
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52643
diff
changeset
|
250 |
val padding_command: Properties.entry |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
251 |
val dialogN: string val dialog: serial -> string -> T |
63681 | 252 |
val jedit_actionN: string |
76394 | 253 |
val function: string -> Properties.entry |
72119
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72116
diff
changeset
|
254 |
val ML_statistics: {pid: int, stats_dir: string} -> Properties.T |
70665
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70499
diff
changeset
|
255 |
val commands_accepted: Properties.T |
52563 | 256 |
val assign_update: Properties.T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
257 |
val removed_versions: Properties.T |
73419
22f3f2117ed7
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents:
72861
diff
changeset
|
258 |
val invoke_scala: string -> string -> Properties.T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
259 |
val cancel_scala: string -> Properties.T |
50975 | 260 |
val task_statistics: Properties.entry |
51216 | 261 |
val command_timing: Properties.entry |
66873
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66379
diff
changeset
|
262 |
val theory_timing: Properties.entry |
72002
5c4800f6b25a
more robust protocol for "Timing ..." messages, notably for pide_session=true;
wenzelm
parents:
71912
diff
changeset
|
263 |
val session_timing: Properties.entry |
50845 | 264 |
val loading_theory: string -> Properties.T |
65313 | 265 |
val build_session_finished: Properties.T |
56864 | 266 |
val print_operations: Properties.T |
69788 | 267 |
val exportN: string |
268 |
type export_args = |
|
269 |
{id: string option, |
|
270 |
serial: serial, |
|
271 |
theory_name: string, |
|
272 |
name: string, |
|
273 |
executable: bool, |
|
70499 | 274 |
compress: bool, |
275 |
strict: bool} |
|
69788 | 276 |
val export: export_args -> Properties.T |
60842 | 277 |
val debugger_state: string -> Properties.T |
60834 | 278 |
val debugger_output: string -> Properties.T |
57594
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
56864
diff
changeset
|
279 |
val simp_trace_panelN: string |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
280 |
val simp_trace_logN: string |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
281 |
val simp_trace_stepN: string |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
282 |
val simp_trace_recurseN: string |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
283 |
val simp_trace_hintN: string |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
284 |
val simp_trace_ignoreN: string |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
285 |
val simp_trace_cancel: serial -> Properties.T |
80858
a392351d1ed4
more robust: global ML name space for markup elements;
wenzelm
parents:
80846
diff
changeset
|
286 |
val code_presentationN: string |
a392351d1ed4
more robust: global ML name space for markup elements;
wenzelm
parents:
80846
diff
changeset
|
287 |
val stmt_nameN: string |
69345
6bd63c94cf62
tuned signature (see also src/Tools/Haskell/Markup.hs);
wenzelm
parents:
69320
diff
changeset
|
288 |
type output = Output.output * Output.output |
6bd63c94cf62
tuned signature (see also src/Tools/Haskell/Markup.hs);
wenzelm
parents:
69320
diff
changeset
|
289 |
val no_output: output |
6bd63c94cf62
tuned signature (see also src/Tools/Haskell/Markup.hs);
wenzelm
parents:
69320
diff
changeset
|
290 |
val output: T -> output |
25552 | 291 |
val markup: T -> string -> string |
59125 | 292 |
val markups: T list -> string -> string |
55956
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55919
diff
changeset
|
293 |
val markup_report: string -> string |
23623 | 294 |
end; |
295 |
||
296 |
structure Markup: MARKUP = |
|
297 |
struct |
|
298 |
||
30221 | 299 |
(** markup elements **) |
300 |
||
23658 | 301 |
(* basic markup *) |
23623 | 302 |
|
28017 | 303 |
type T = string * Properties.T; |
23637 | 304 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
305 |
val empty = ("", []); |
23637 | 306 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
307 |
fun is_empty ("", _) = true |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
308 |
| is_empty _ = false; |
27883 | 309 |
|
23794 | 310 |
|
23671 | 311 |
fun properties more_props ((elem, props): T) = |
28017 | 312 |
(elem, fold_rev Properties.put more_props props); |
23671 | 313 |
|
55551 | 314 |
fun markup_elem name = (name, (name, []): T); |
315 |
fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T); |
|
63806 | 316 |
fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T); |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
317 |
|
26977 | 318 |
|
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
319 |
(* misc properties *) |
26977 | 320 |
|
23658 | 321 |
val nameN = "name"; |
27818 | 322 |
fun name a = properties [(nameN, a)]; |
78463
c956b43749f0
clarified signature: systematic use of Properties.make_string;
wenzelm
parents:
78279
diff
changeset
|
323 |
val name_proper = Properties.make_string nameN; |
27818 | 324 |
|
68997 | 325 |
val xnameN = "xname"; |
326 |
fun xname a = properties [(xnameN, a)]; |
|
327 |
||
23658 | 328 |
val kindN = "kind"; |
78463
c956b43749f0
clarified signature: systematic use of Properties.make_string;
wenzelm
parents:
78279
diff
changeset
|
329 |
fun kind a = properties [(kindN, a)]; |
c956b43749f0
clarified signature: systematic use of Properties.make_string;
wenzelm
parents:
78279
diff
changeset
|
330 |
val kind_proper = Properties.make_string kindN; |
23671 | 331 |
|
60744 | 332 |
val serialN = "serial"; |
63806 | 333 |
fun serial_properties i = [(serialN, Value.print_int i)]; |
60744 | 334 |
|
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
335 |
val instanceN = "instance"; |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
336 |
|
23658 | 337 |
|
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69916
diff
changeset
|
338 |
(* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *) |
69889
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
339 |
|
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
340 |
val (meta_titleN, meta_title) = markup_elem "meta_title"; |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
341 |
val (meta_creatorN, meta_creator) = markup_elem "meta_creator"; |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
342 |
val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor"; |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
343 |
val (meta_dateN, meta_date) = markup_elem "meta_date"; |
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69916
diff
changeset
|
344 |
val (meta_licenseN, meta_license) = markup_elem "meta_license"; |
69889
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
345 |
val (meta_descriptionN, meta_description) = markup_elem "meta_description"; |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
346 |
|
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
347 |
|
55550 | 348 |
(* embedded languages *) |
349 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
350 |
val languageN = "language"; |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55613
diff
changeset
|
351 |
val symbolsN = "symbols"; |
55666 | 352 |
val antiquotesN = "antiquotes"; |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
353 |
val delimitedN = "delimited" |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
354 |
|
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
355 |
fun is_delimited props = |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
356 |
Properties.get props delimitedN = SOME "true"; |
55666 | 357 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
358 |
fun language {name, symbols, antiquotes, delimited} = |
55666 | 359 |
(languageN, |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
360 |
[(nameN, name), |
63806 | 361 |
(symbolsN, Value.print_bool symbols), |
362 |
(antiquotesN, Value.print_bool antiquotes), |
|
363 |
(delimitedN, Value.print_bool delimited)]); |
|
55550 | 364 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
365 |
fun language' {name, symbols, antiquotes} delimited = |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
366 |
language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
367 |
|
62231
25f4a9cd8b68
tuned markup, e.g. relevant for Rendering.tooltip;
wenzelm
parents:
61864
diff
changeset
|
368 |
val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false}; |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
369 |
val language_method = |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
370 |
language {name = "method", symbols = true, antiquotes = false, delimited = false}; |
56033 | 371 |
val language_attribute = |
372 |
language {name = "attribute", symbols = true, antiquotes = false, delimited = false}; |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
373 |
val language_sort = language' {name = "sort", symbols = true, antiquotes = false}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
374 |
val language_type = language' {name = "type", symbols = true, antiquotes = false}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
375 |
val language_term = language' {name = "term", symbols = true, antiquotes = false}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
376 |
val language_prop = language' {name = "prop", symbols = true, antiquotes = false}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
377 |
val language_ML = language' {name = "ML", symbols = false, antiquotes = true}; |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
378 |
val language_SML = language' {name = "SML", symbols = false, antiquotes = false}; |
61600
1ca11ddfcc70
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
wenzelm
parents:
61598
diff
changeset
|
379 |
val language_document = language' {name = "document", symbols = false, antiquotes = true}; |
69887 | 380 |
val language_document_marker = |
381 |
language {name = "document_marker", symbols = true, antiquotes = true, delimited = true}; |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
382 |
val language_antiquotation = |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
383 |
language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
384 |
val language_text = language' {name = "text", symbols = true, antiquotes = false}; |
62772 | 385 |
val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false}; |
67429 | 386 |
val language_latex = language' {name = "latex", symbols = false, antiquotes = false}; |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
387 |
val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true}; |
72841 | 388 |
val language_path = language' {name = "path", symbols = false, antiquotes = false}; |
72843 | 389 |
val language_url = language' {name = "url", symbols = false, antiquotes = false}; |
62772 | 390 |
val language_mixfix = |
391 |
language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true}; |
|
55550 | 392 |
|
393 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
394 |
(* formal entities *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
395 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
396 |
val (bindingN, binding) = markup_elem "binding"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
397 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
398 |
val entityN = "entity"; |
78463
c956b43749f0
clarified signature: systematic use of Properties.make_string;
wenzelm
parents:
78279
diff
changeset
|
399 |
fun entity kind name = (entityN, name_proper name @ kind_proper kind); |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
400 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
401 |
val defN = "def"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
402 |
val refN = "ref"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
403 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
404 |
|
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
405 |
(* completion *) |
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
406 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
407 |
val (completionN, completion) = markup_elem "completion"; |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55837
diff
changeset
|
408 |
val (no_completionN, no_completion) = markup_elem "no_completion"; |
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
409 |
|
69557 | 410 |
val (updateN, update) = markup_elem "update"; |
411 |
||
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
412 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
413 |
(* position *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
414 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
415 |
val lineN = "line"; |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58855
diff
changeset
|
416 |
val end_lineN = "end_line"; |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58855
diff
changeset
|
417 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
418 |
val offsetN = "offset"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
419 |
val end_offsetN = "end_offset"; |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58855
diff
changeset
|
420 |
|
78021 | 421 |
val labelN = "label"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
422 |
val fileN = "file"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
423 |
val idN = "id"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
424 |
|
74182 | 425 |
val (positionN, position) = markup_elem "position"; |
426 |
||
78021 | 427 |
val position_properties = [lineN, offsetN, end_offsetN, labelN, fileN, idN]; |
72708 | 428 |
fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry); |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
429 |
|
74182 | 430 |
|
431 |
(* position "def" names *) |
|
432 |
||
433 |
fun make_def a = "def_" ^ a; |
|
434 |
||
435 |
val def_names = Symtab.make (map (fn a => (a, make_def a)) position_properties); |
|
436 |
||
437 |
fun def_name a = |
|
438 |
(case Symtab.lookup def_names a of |
|
439 |
SOME b => b |
|
440 |
| NONE => make_def a); |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
441 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
442 |
|
80911
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
443 |
(* notation: mixfix annotations *) |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
444 |
|
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
445 |
val notation_mixfixN = "mixfix"; |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
446 |
val notation_infixN = "infix"; |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
447 |
val notation_binderN = "binder"; |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
448 |
val notations = [notation_mixfixN, notation_infixN, notation_binderN]; |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
449 |
|
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
450 |
val notationN = "notation"; |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
451 |
fun notation {kind, name} = (notationN, kind_proper kind @ name_proper name); |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
452 |
|
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
453 |
val notation0 = (notationN, []); |
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
454 |
|
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
455 |
|
58464 | 456 |
(* expression *) |
457 |
||
62806 | 458 |
val expressionN = "expression"; |
78463
c956b43749f0
clarified signature: systematic use of Properties.make_string;
wenzelm
parents:
78279
diff
changeset
|
459 |
fun expression kind = (expressionN, kind_proper kind); |
58464 | 460 |
|
80909 | 461 |
val expression0 = (expressionN, []); |
462 |
||
58464 | 463 |
|
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
464 |
(* citation *) |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
465 |
|
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
466 |
val (citationN, citation) = markup_string "citation" nameN; |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
467 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
468 |
|
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
469 |
(* external resources *) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
470 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
471 |
val (pathN, path) = markup_string "path" nameN; |
70016 | 472 |
val (export_pathN, export_path) = markup_string "export_path" nameN; |
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
473 |
val (urlN, url) = markup_string "url" nameN; |
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61614
diff
changeset
|
474 |
val (docN, doc) = markup_string "doc" nameN; |
72763 | 475 |
val (toolN, tool) = markup_string "tool" nameN; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
476 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
477 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
478 |
(* pretty printing *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
479 |
|
62783 | 480 |
val markupN = "markup"; |
62786 | 481 |
val consistentN = "consistent"; |
62789 | 482 |
val unbreakableN = "unbreakable"; |
62786 | 483 |
val indentN = "indent"; |
484 |
||
80911
8ad5e6df050b
block markup for specific notation, notably infix and binder;
wenzelm
parents:
80909
diff
changeset
|
485 |
val block_properties = [notationN, expressionN, markupN, consistentN, unbreakableN, indentN]; |
62786 | 486 |
|
61864 | 487 |
val widthN = "width"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
488 |
|
61864 | 489 |
val blockN = "block"; |
490 |
fun block c i = |
|
491 |
(blockN, |
|
63806 | 492 |
(if c then [(consistentN, Value.print_bool c)] else []) @ |
493 |
(if i <> 0 then [(indentN, Value.print_int i)] else [])); |
|
61864 | 494 |
|
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
495 |
val breakN = "break"; |
61864 | 496 |
fun break w i = |
497 |
(breakN, |
|
63806 | 498 |
(if w <> 0 then [(widthN, Value.print_int w)] else []) @ |
499 |
(if i <> 0 then [(indentN, Value.print_int i)] else [])); |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
500 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
501 |
val (fbreakN, fbreak) = markup_elem "fbreak"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
502 |
|
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51228
diff
changeset
|
503 |
val (itemN, item) = markup_elem "item"; |
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51228
diff
changeset
|
504 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
505 |
|
56548 | 506 |
(* text properties *) |
507 |
||
508 |
val (wordsN, words) = markup_elem "words"; |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
509 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
510 |
val (hiddenN, hidden) = markup_elem "hidden"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
511 |
|
68298
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68101
diff
changeset
|
512 |
val (deleteN, delete) = markup_elem "delete"; |
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68101
diff
changeset
|
513 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
514 |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57975
diff
changeset
|
515 |
(* misc entities *) |
56465 | 516 |
|
74671 | 517 |
val load_commandN = "load_command"; |
71912 | 518 |
val bash_functionN = "bash_function"; |
77028
f5896dea6fce
more direct check of bibtex entries via Isabelle/Scala;
wenzelm
parents:
76957
diff
changeset
|
519 |
val bibtex_entryN = "bibtex_entry"; |
71912 | 520 |
val scala_functionN = "scala_function"; |
56465 | 521 |
val system_optionN = "system_option"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
522 |
|
67219 | 523 |
val sessionN = "session"; |
524 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
525 |
val theoryN = "theory"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
526 |
val classN = "class"; |
74112 | 527 |
val localeN = "locale"; |
74261
d28a51dd9da6
export other entities, e.g. relevant for formal document output;
wenzelm
parents:
74182
diff
changeset
|
528 |
val bundleN = "bundle"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
529 |
val type_nameN = "type_name"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
530 |
val constantN = "constant"; |
74112 | 531 |
val axiomN = "axiom"; |
532 |
val factN = "fact"; |
|
533 |
val oracleN = "oracle"; |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
534 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
535 |
val (fixedN, fixed) = markup_string "fixed" nameN; |
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53055
diff
changeset
|
536 |
val (caseN, case_) = markup_string "case" nameN; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
537 |
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; |
63337 | 538 |
val (literal_factN, literal_fact) = markup_string "literal_fact" nameN; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
539 |
|
74112 | 540 |
val attributeN = "attribute"; |
541 |
val methodN = "method"; |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57975
diff
changeset
|
542 |
val method_modifierN = "method_modifier"; |
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57975
diff
changeset
|
543 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
544 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
545 |
(* inner syntax *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
546 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
547 |
val (tfreeN, tfree) = markup_elem "tfree"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
548 |
val (tvarN, tvar) = markup_elem "tvar"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
549 |
val (freeN, free) = markup_elem "free"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
550 |
val (skolemN, skolem) = markup_elem "skolem"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
551 |
val (boundN, bound) = markup_elem "bound"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
552 |
val (varN, var) = markup_elem "var"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
553 |
val (numeralN, numeral) = markup_elem "numeral"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
554 |
val (literalN, literal) = markup_elem "literal"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
555 |
val (delimiterN, delimiter) = markup_elem "delimiter"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
556 |
val (inner_stringN, inner_string) = markup_elem "inner_string"; |
55033 | 557 |
val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
558 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
559 |
val (token_rangeN, token_range) = markup_elem "token_range"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
560 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
561 |
val (sortingN, sorting) = markup_elem "sorting"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
562 |
val (typingN, typing) = markup_elem "typing"; |
63347 | 563 |
val (class_parameterN, class_parameter) = markup_elem "class_parameter"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
564 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
565 |
|
60744 | 566 |
(* ML *) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
567 |
|
55505 | 568 |
val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1"; |
569 |
val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2"; |
|
570 |
val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3"; |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
571 |
val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
572 |
val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
573 |
val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
574 |
val (ML_charN, ML_char) = markup_elem "ML_char"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
575 |
val (ML_stringN, ML_string) = markup_elem "ML_string"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
576 |
val (ML_commentN, ML_comment) = markup_elem "ML_comment"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
577 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
578 |
val ML_defN = "ML_def"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
579 |
val ML_openN = "ML_open"; |
55837 | 580 |
val ML_structureN = "ML_structure"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
581 |
val (ML_typingN, ML_typing) = markup_elem "ML_typing"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
582 |
|
60744 | 583 |
val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN; |
584 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
585 |
|
55550 | 586 |
(* antiquotations *) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
587 |
|
55526 | 588 |
val (antiquotedN, antiquoted) = markup_elem "antiquoted"; |
589 |
val (antiquoteN, antiquote) = markup_elem "antiquote"; |
|
590 |
||
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69345
diff
changeset
|
591 |
val file_typeN = "file_type"; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69345
diff
changeset
|
592 |
val antiquotationN = "antiquotation"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
593 |
val ML_antiquotationN = "ML_antiquotation"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
594 |
val document_antiquotationN = "document_antiquotation"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
595 |
val document_antiquotation_optionN = "document_antiquotation_option"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
596 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
597 |
|
70135
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70016
diff
changeset
|
598 |
(* document text *) |
69965
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69962
diff
changeset
|
599 |
|
76514
2615cf68f6f4
ML support for the Prism.js syntax highlighter -- via Isabelle/Scala;
wenzelm
parents:
76394
diff
changeset
|
600 |
val prismjs_languageN = "prismjs_language"; |
2615cf68f6f4
ML support for the Prism.js syntax highlighter -- via Isabelle/Scala;
wenzelm
parents:
76394
diff
changeset
|
601 |
|
69965
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69962
diff
changeset
|
602 |
val (raw_textN, raw_text) = markup_elem "raw_text"; |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69962
diff
changeset
|
603 |
val (plain_textN, plain_text) = markup_elem "plain_text"; |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69962
diff
changeset
|
604 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
605 |
val (paragraphN, paragraph) = markup_elem "paragraph"; |
50545
00bdc48c5f71
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
wenzelm
parents:
50543
diff
changeset
|
606 |
val (text_foldN, text_fold) = markup_elem "text_fold"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
607 |
|
70229 | 608 |
val (document_markerN, document_marker) = markup_elem "document_marker"; |
70135
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70016
diff
changeset
|
609 |
val (document_tagN, document_tag) = markup_string "document_tag" nameN; |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70016
diff
changeset
|
610 |
|
74784
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74673
diff
changeset
|
611 |
|
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74673
diff
changeset
|
612 |
(* LaTeX *) |
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74673
diff
changeset
|
613 |
|
73780
466fae6bf22e
compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents:
73419
diff
changeset
|
614 |
val (document_latexN, document_latex) = markup_elem "document_latex"; |
466fae6bf22e
compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents:
73419
diff
changeset
|
615 |
|
74784
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74673
diff
changeset
|
616 |
val (latex_outputN, latex_output) = markup_elem "latex_output"; |
74790 | 617 |
val (latex_macro0N, latex_macro0) = markup_string "latex_macro0" nameN; |
618 |
val (latex_macroN, latex_macro) = markup_string "latex_macro" nameN; |
|
619 |
val (latex_environmentN, latex_environment) = markup_string "latex_environment" nameN; |
|
74823 | 620 |
val (latex_headingN, latex_heading) = markup_string "latex_heading" kindN; |
621 |
val (latex_bodyN, latex_body) = markup_string "latex_body" kindN; |
|
76955 | 622 |
val (latex_citeN, _) = markup_elem "latex_cite"; |
76957
deb7dffb3340
avoid confusion of markup element vs. property names;
wenzelm
parents:
76956
diff
changeset
|
623 |
fun latex_cite {kind, citations} = |
78463
c956b43749f0
clarified signature: systematic use of Properties.make_string;
wenzelm
parents:
78279
diff
changeset
|
624 |
(latex_citeN, kind_proper kind @ Properties.make_string "citations" citations); |
74786 | 625 |
val (latex_index_itemN, latex_index_item) = markup_elem "latex_index_item"; |
626 |
val (latex_index_entryN, latex_index_entry) = markup_string "latex_index_entry" kindN; |
|
74826
0e4d8aa61ad7
more symbolic latex_output via XML (using YXML within text);
wenzelm
parents:
74823
diff
changeset
|
627 |
val (latex_delimN, latex_delim) = markup_string "latex_delim" nameN; |
0e4d8aa61ad7
more symbolic latex_output via XML (using YXML within text);
wenzelm
parents:
74823
diff
changeset
|
628 |
val (latex_tagN, latex_tag) = markup_string "latex_tag" nameN; |
74784
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74673
diff
changeset
|
629 |
|
74836
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
74826
diff
changeset
|
630 |
val optional_argumentN = "optional_argument"; |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
74826
diff
changeset
|
631 |
fun optional_argument arg = properties [(optional_argumentN, arg)]; |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
74826
diff
changeset
|
632 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
633 |
|
61449 | 634 |
(* Markdown document structure *) |
635 |
||
636 |
val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph"; |
|
67323
d02208cefbdb
PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
wenzelm
parents:
67322
diff
changeset
|
637 |
val (markdown_itemN, markdown_item) = markup_elem "markdown_item"; |
67336 | 638 |
val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth"; |
61449 | 639 |
val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN; |
67336 | 640 |
|
641 |
val itemizeN = "itemize"; |
|
642 |
val enumerateN = "enumerate"; |
|
643 |
val descriptionN = "description"; |
|
61449 | 644 |
|
645 |
||
59795 | 646 |
(* formal input *) |
647 |
||
648 |
val inputN = "input"; |
|
63806 | 649 |
fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props); |
59795 | 650 |
|
651 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
652 |
(* outer syntax *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
653 |
|
59935 | 654 |
val (command_keywordN, command_keyword) = markup_elem "command_keyword"; |
78279
dab089b25eb6
more markup for command_span: this allows to reconstruct Thy_Element structure without knowing the outer syntax;
wenzelm
parents:
78021
diff
changeset
|
655 |
|
dab089b25eb6
more markup for command_span: this allows to reconstruct Thy_Element structure without knowing the outer syntax;
wenzelm
parents:
78021
diff
changeset
|
656 |
val command_spanN = "command_span"; |
78463
c956b43749f0
clarified signature: systematic use of Properties.make_string;
wenzelm
parents:
78279
diff
changeset
|
657 |
fun command_span {name, kind} : T = (command_spanN, name_proper name @ kind_proper kind); |
66044 | 658 |
|
66066 | 659 |
val commandN = "command"; val command_properties = properties [(kindN, commandN)]; |
660 |
val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)]; |
|
661 |
||
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
662 |
val (keyword1N, keyword1) = markup_elem "keyword1"; |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
663 |
val (keyword2N, keyword2) = markup_elem "keyword2"; |
55763 | 664 |
val (keyword3N, keyword3) = markup_elem "keyword3"; |
55919
2eb8c13339a5
more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
wenzelm
parents:
55914
diff
changeset
|
665 |
val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword"; |
56202 | 666 |
val (improperN, improper) = markup_elem "improper"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
667 |
val (operatorN, operator) = markup_elem "operator"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
668 |
val (stringN, string) = markup_elem "string"; |
59081 | 669 |
val (alt_stringN, alt_string) = markup_elem "alt_string"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
670 |
val (verbatimN, verbatim) = markup_elem "verbatim"; |
55033 | 671 |
val (cartoucheN, cartouche) = markup_elem "cartouche"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
672 |
val (commentN, comment) = markup_elem "comment"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
673 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
674 |
|
69320 | 675 |
(* comments *) |
676 |
||
677 |
val (comment1N, comment1) = markup_elem "comment1"; |
|
678 |
val (comment2N, comment2) = markup_elem "comment2"; |
|
679 |
val (comment3N, comment3) = markup_elem "comment3"; |
|
680 |
||
681 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
682 |
(* timing *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
683 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
684 |
val elapsedN = "elapsed"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
685 |
val cpuN = "cpu"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
686 |
val gcN = "gc"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
687 |
|
50781 | 688 |
fun timing_properties {elapsed, cpu, gc} = |
67000
1698e9ccef2d
more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
wenzelm
parents:
66873
diff
changeset
|
689 |
[(elapsedN, Value.print_time elapsed), |
1698e9ccef2d
more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
wenzelm
parents:
66873
diff
changeset
|
690 |
(cpuN, Value.print_time cpu), |
1698e9ccef2d
more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
wenzelm
parents:
66873
diff
changeset
|
691 |
(gcN, Value.print_time gc)]; |
50781 | 692 |
|
51665 | 693 |
val timingN = "timing"; |
694 |
fun timing t = (timingN, timing_properties t); |
|
51218
6425a0d3b7ac
support for build passing timings from Scala to ML;
wenzelm
parents:
51217
diff
changeset
|
695 |
|
51228 | 696 |
|
697 |
(* command timing *) |
|
698 |
||
699 |
fun parse_command_timing_properties props = |
|
700 |
(case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of |
|
701 |
(SOME file, SOME offset, SOME name) => |
|
63806 | 702 |
SOME ({file = file, offset = Value.parse_int offset, name = name}, |
77772 | 703 |
Properties.get_seconds props elapsedN) |
51228 | 704 |
| _ => NONE); |
705 |
||
706 |
||
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
707 |
(* indentation *) |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
708 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
709 |
val (command_indentN, command_indent) = markup_int "command_indent" indentN; |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
710 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
711 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
712 |
(* goals *) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
713 |
|
50543 | 714 |
val (goalN, goal) = markup_elem "goal"; |
50537
08ce81aeeacc
more subgoal markup information, which is potentially useful to manage proof state output;
wenzelm
parents:
50503
diff
changeset
|
715 |
val (subgoalN, subgoal) = markup_string "subgoal" nameN; |
50215 | 716 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50255
diff
changeset
|
717 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
718 |
(* command status *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
719 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
720 |
val taskN = "task"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
721 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
722 |
val (forkedN, forked) = markup_elem "forked"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
723 |
val (joinedN, joined) = markup_elem "joined"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
724 |
val (runningN, running) = markup_elem "running"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
725 |
val (finishedN, finished) = markup_elem "finished"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
726 |
val (failedN, failed) = markup_elem "failed"; |
68871
f5c76072db55
more explicit status for "canceled" command within theory node;
wenzelm
parents:
68822
diff
changeset
|
727 |
val (canceledN, canceled) = markup_elem "canceled"; |
68323 | 728 |
val (initializedN, initialized) = markup_elem "initialized"; |
68884
9b97d0b20d95
clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents:
68871
diff
changeset
|
729 |
val (finalizedN, finalized) = markup_elem "finalized"; |
70780
034742453594
more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents:
70665
diff
changeset
|
730 |
val (consolidatingN, consolidating) = markup_elem "consolidating"; |
66379
6392766f3c25
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents:
66066
diff
changeset
|
731 |
val (consolidatedN, consolidated) = markup_elem "consolidated"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
732 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
733 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
734 |
(* messages *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
735 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50845
diff
changeset
|
736 |
val exec_idN = "exec_id"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
737 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
738 |
val initN = "init"; |
61209 | 739 |
val (statusN, status) = markup_elem "status"; |
740 |
val (resultN, result) = markup_elem "result"; |
|
741 |
val (writelnN, writeln) = markup_elem "writeln"; |
|
742 |
val (stateN, state) = markup_elem "state" |
|
743 |
val (informationN, information) = markup_elem "information"; |
|
744 |
val (tracingN, tracing) = markup_elem "tracing"; |
|
745 |
val (warningN, warning) = markup_elem "warning"; |
|
746 |
val (legacyN, legacy) = markup_elem "legacy"; |
|
747 |
val (errorN, error) = markup_elem "error"; |
|
748 |
val (systemN, system) = markup_elem "system"; |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
749 |
val protocolN = "protocol"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
750 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
751 |
val (reportN, report) = markup_elem "report"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
752 |
val (no_reportN, no_report) = markup_elem "no_report"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
753 |
|
64677
8dc24130e8fe
more uniform treatment of "bad" like other messages (with serial number);
wenzelm
parents:
63806
diff
changeset
|
754 |
val badN = "bad"; |
8dc24130e8fe
more uniform treatment of "bad" like other messages (with serial number);
wenzelm
parents:
63806
diff
changeset
|
755 |
fun bad () = (badN, serial_properties (serial ())); |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
756 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
757 |
val (intensifyN, intensify) = markup_elem "intensify"; |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
758 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
759 |
|
73835 | 760 |
(* ML profiling *) |
761 |
||
762 |
val countN = "count"; |
|
763 |
||
764 |
val ML_profiling_entryN = "ML_profiling_entry"; |
|
765 |
fun ML_profiling_entry {name, count} = |
|
766 |
(ML_profiling_entryN, [(nameN, name), (countN, Value.print_int count)]); |
|
767 |
||
768 |
val (ML_profilingN, ML_profiling) = markup_string "ML_profiling" kindN; |
|
769 |
||
770 |
||
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
771 |
(* active areas *) |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
772 |
|
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50683
diff
changeset
|
773 |
val browserN = "browser" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
774 |
val graphviewN = "graphview"; |
69650 | 775 |
val theory_exportsN = "theory_exports"; |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
776 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
777 |
val sendbackN = "sendback"; |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
778 |
val paddingN = "padding"; |
52697
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52643
diff
changeset
|
779 |
val padding_line = (paddingN, "line"); |
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52643
diff
changeset
|
780 |
val padding_command = (paddingN, "command"); |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
781 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
782 |
val dialogN = "dialog"; |
63806 | 783 |
fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]); |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
784 |
|
63681 | 785 |
val jedit_actionN = "jedit_action"; |
786 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
787 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
788 |
(* protocol message functions *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
789 |
|
76394 | 790 |
fun function name = ("function", name); |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
791 |
|
72119
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72116
diff
changeset
|
792 |
fun ML_statistics {pid, stats_dir} = |
76394 | 793 |
[function "ML_statistics", ("pid", Value.print_int pid), ("stats_dir", stats_dir)]; |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72106
diff
changeset
|
794 |
|
76394 | 795 |
val commands_accepted = [function "commands_accepted"]; |
70665
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70499
diff
changeset
|
796 |
|
76394 | 797 |
val assign_update = [function "assign_update"]; |
798 |
val removed_versions = [function "removed_versions"]; |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
799 |
|
76394 | 800 |
fun invoke_scala name id = [function "invoke_scala", (nameN, name), (idN, id)]; |
72332
319dd5c618a5
allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents:
72156
diff
changeset
|
801 |
|
76394 | 802 |
fun cancel_scala id = [function "cancel_scala", (idN, id)]; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
803 |
|
76394 | 804 |
val task_statistics = function "task_statistics"; |
50975 | 805 |
|
76394 | 806 |
val command_timing = function "command_timing"; |
51216 | 807 |
|
76394 | 808 |
val theory_timing = function "theory_timing"; |
66873
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66379
diff
changeset
|
809 |
|
76394 | 810 |
val session_timing = function "session_timing"; |
72002
5c4800f6b25a
more robust protocol for "Timing ..." messages, notably for pide_session=true;
wenzelm
parents:
71912
diff
changeset
|
811 |
|
76394 | 812 |
fun loading_theory name = [function "loading_theory", (nameN, name)]; |
50845 | 813 |
|
76394 | 814 |
val build_session_finished = [function "build_session_finished"]; |
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
815 |
|
76394 | 816 |
val print_operations = [function "print_operations"]; |
56864 | 817 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
818 |
|
69788 | 819 |
(* export *) |
820 |
||
821 |
val exportN = "export"; |
|
822 |
||
823 |
type export_args = |
|
824 |
{id: string option, |
|
825 |
serial: serial, |
|
826 |
theory_name: string, |
|
827 |
name: string, |
|
828 |
executable: bool, |
|
70499 | 829 |
compress: bool, |
830 |
strict: bool}; |
|
69788 | 831 |
|
70499 | 832 |
fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) = |
76394 | 833 |
[function exportN, |
69788 | 834 |
(idN, the_default "" id), |
835 |
(serialN, Value.print_int serial), |
|
836 |
("theory_name", theory_name), |
|
837 |
(nameN, name), |
|
838 |
("executable", Value.print_bool executable), |
|
70499 | 839 |
("compress", Value.print_bool compress), |
840 |
("strict", Value.print_bool strict)]; |
|
69788 | 841 |
|
842 |
||
60830 | 843 |
(* debugger *) |
844 |
||
76394 | 845 |
fun debugger_state name = [function "debugger_state", (nameN, name)]; |
846 |
fun debugger_output name = [function "debugger_output", (nameN, name)]; |
|
60830 | 847 |
|
848 |
||
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
849 |
(* simplifier trace *) |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
850 |
|
57594
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
56864
diff
changeset
|
851 |
val simp_trace_panelN = "simp_trace_panel"; |
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
56864
diff
changeset
|
852 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
853 |
val simp_trace_logN = "simp_trace_log"; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
854 |
val simp_trace_stepN = "simp_trace_step"; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
855 |
val simp_trace_recurseN = "simp_trace_recurse"; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
856 |
val simp_trace_hintN = "simp_trace_hint"; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
857 |
val simp_trace_ignoreN = "simp_trace_ignore"; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
858 |
|
76394 | 859 |
fun simp_trace_cancel i = [function "simp_trace_cancel", (serialN, Value.print_int i)]; |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
860 |
|
27969 | 861 |
|
80858
a392351d1ed4
more robust: global ML name space for markup elements;
wenzelm
parents:
80846
diff
changeset
|
862 |
(* code generator *) |
a392351d1ed4
more robust: global ML name space for markup elements;
wenzelm
parents:
80846
diff
changeset
|
863 |
|
a392351d1ed4
more robust: global ML name space for markup elements;
wenzelm
parents:
80846
diff
changeset
|
864 |
val code_presentationN = "code_presentation"; |
a392351d1ed4
more robust: global ML name space for markup elements;
wenzelm
parents:
80846
diff
changeset
|
865 |
val stmt_nameN = "stmt_name"; |
a392351d1ed4
more robust: global ML name space for markup elements;
wenzelm
parents:
80846
diff
changeset
|
866 |
|
a392351d1ed4
more robust: global ML name space for markup elements;
wenzelm
parents:
80846
diff
changeset
|
867 |
|
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
868 |
|
80861
9de19e3a7231
dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE";
wenzelm
parents:
80858
diff
changeset
|
869 |
(** output depending on print_mode **) |
23704 | 870 |
|
69345
6bd63c94cf62
tuned signature (see also src/Tools/Haskell/Markup.hs);
wenzelm
parents:
69320
diff
changeset
|
871 |
type output = Output.output * Output.output; |
6bd63c94cf62
tuned signature (see also src/Tools/Haskell/Markup.hs);
wenzelm
parents:
69320
diff
changeset
|
872 |
|
29325 | 873 |
val no_output = ("", ""); |
23704 | 874 |
|
80861
9de19e3a7231
dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE";
wenzelm
parents:
80858
diff
changeset
|
875 |
fun output m = |
80867 | 876 |
if not (is_empty m) andalso Print_Mode.PIDE_enabled () |
80861
9de19e3a7231
dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE";
wenzelm
parents:
80858
diff
changeset
|
877 |
then YXML.output_markup m else no_output; |
23704 | 878 |
|
80846
9ed32b8a03a9
clarified print mode "latex": no longer impact Output/Markup/Pretty operations;
wenzelm
parents:
80827
diff
changeset
|
879 |
fun markup m = output m |-> Library.enclose; |
25552 | 880 |
|
59125 | 881 |
val markups = fold_rev markup; |
882 |
||
55956
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55919
diff
changeset
|
883 |
fun markup_report "" = "" |
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55919
diff
changeset
|
884 |
| markup_report txt = markup report txt; |
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55919
diff
changeset
|
885 |
|
23704 | 886 |
end; |