author | wenzelm |
Tue, 30 Dec 2014 23:45:03 +0100 | |
changeset 59203 | 5f0bd5afc16d |
parent 59184 | 830bb7ddb3ab |
child 59364 | 3b5da177ae6b |
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 |
|
51951
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51665
diff
changeset
|
9 |
val parse_bool: string -> bool |
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51665
diff
changeset
|
10 |
val print_bool: bool -> string |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
11 |
val parse_int: string -> int |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
12 |
val print_int: int -> string |
51988 | 13 |
val parse_real: string -> real |
14 |
val print_real: real -> string |
|
28017 | 15 |
type T = string * Properties.T |
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
16 |
val empty: T |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
17 |
val is_empty: T -> bool |
38229 | 18 |
val properties: Properties.T -> T -> T |
23623 | 19 |
val nameN: string |
27818 | 20 |
val name: string -> T -> T |
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38871
diff
changeset
|
21 |
val kindN: string |
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
22 |
val instanceN: string |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
23 |
val languageN: string |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55613
diff
changeset
|
24 |
val symbolsN: string |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
25 |
val delimitedN: string |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
26 |
val is_delimited: Properties.T -> bool |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
27 |
val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
28 |
val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T |
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55750
diff
changeset
|
29 |
val language_method: T |
56033 | 30 |
val language_attribute: T |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
31 |
val language_sort: bool -> T |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
32 |
val language_type: bool -> T |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
33 |
val language_term: bool -> T |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
34 |
val language_prop: bool -> T |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
35 |
val language_ML: bool -> T |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
36 |
val language_SML: bool -> T |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
37 |
val language_document: bool -> T |
55653
528de9a20054
more markup -- complete symbols within antiquotation, notably with broken arguments;
wenzelm
parents:
55615
diff
changeset
|
38 |
val language_antiquotation: T |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
39 |
val language_text: bool -> T |
55613 | 40 |
val language_rail: T |
56034
1c59b555ac4a
some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
wenzelm
parents:
56033
diff
changeset
|
41 |
val language_path: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
42 |
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
|
43 |
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
|
44 |
val get_entity_kind: T -> string option |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
45 |
val defN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
46 |
val refN: string |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
47 |
val completionN: string val completion: T |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55837
diff
changeset
|
48 |
val no_completionN: string val no_completion: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
49 |
val lineN: string |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58855
diff
changeset
|
50 |
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
|
51 |
val offsetN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
52 |
val end_offsetN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
53 |
val fileN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
54 |
val idN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
55 |
val position_properties': string list |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
56 |
val position_properties: string list |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
57 |
val positionN: string val position: T |
58464 | 58 |
val expressionN: string val expression: T |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
59 |
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
|
60 |
val pathN: string val path: string -> T |
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
61 |
val urlN: string val url: string -> T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
62 |
val indentN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
63 |
val blockN: string val block: int -> T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
64 |
val widthN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
65 |
val breakN: string val break: int -> T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
66 |
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
|
67 |
val itemN: string val item: T |
56548 | 68 |
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
|
69 |
val hiddenN: string val hidden: T |
56465 | 70 |
val system_optionN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
71 |
val theoryN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
72 |
val classN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
73 |
val type_nameN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
74 |
val constantN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
75 |
val fixedN: string val fixed: string -> T |
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53055
diff
changeset
|
76 |
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
|
77 |
val dynamic_factN: string val dynamic_fact: string -> T |
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57975
diff
changeset
|
78 |
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
|
79 |
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
|
80 |
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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
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
|
86 |
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
|
87 |
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
|
88 |
val inner_stringN: string val inner_string: T |
55033 | 89 |
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
|
90 |
val inner_commentN: string val inner_comment: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
91 |
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
|
92 |
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
|
93 |
val typingN: string val typing: T |
55505 | 94 |
val ML_keyword1N: string val ML_keyword1: T |
95 |
val ML_keyword2N: string val ML_keyword2: T |
|
96 |
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
|
97 |
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
|
98 |
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
|
99 |
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
|
100 |
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
|
101 |
val ML_stringN: string val ML_string: T |
59112 | 102 |
val ML_cartoucheN: string val ML_cartouche: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
103 |
val ML_commentN: string val ML_comment: T |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
104 |
val SML_stringN: string val SML_string: T |
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
105 |
val SML_commentN: string val SML_comment: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
106 |
val ML_defN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
107 |
val ML_openN: string |
55837 | 108 |
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
|
109 |
val ML_typingN: string val ML_typing: T |
55526 | 110 |
val antiquotedN: string val antiquoted: T |
111 |
val antiquoteN: string val antiquote: T |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
112 |
val ML_antiquotationN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
113 |
val document_antiquotationN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
114 |
val document_antiquotation_optionN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
115 |
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
|
116 |
val text_foldN: string val text_fold: T |
55750
baa7a1e57f4a
back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;
wenzelm
parents:
55744
diff
changeset
|
117 |
val commandN: string val command: T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
118 |
val stringN: string val string: T |
59081 | 119 |
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
|
120 |
val verbatimN: string val verbatim: T |
55033 | 121 |
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
|
122 |
val commentN: string val comment: T |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
123 |
val tokenN: string val token: bool -> Properties.T -> T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
124 |
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
|
125 |
val keyword2N: string val keyword2: T |
55763 | 126 |
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
|
127 |
val quasi_keywordN: string val quasi_keyword: T |
56202 | 128 |
val improperN: string val improper: T |
129 |
val operatorN: string val operator: T |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
130 |
val elapsedN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
131 |
val cpuN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
132 |
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
|
133 |
val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T |
2843cc095a57
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51570
diff
changeset
|
134 |
val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time} |
51228 | 135 |
val command_timingN: string |
136 |
val command_timing_properties: |
|
137 |
{file: string, offset: int, name: string} -> Time.time -> Properties.T |
|
138 |
val parse_command_timing_properties: |
|
139 |
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
|
140 |
val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
141 |
val subgoalsN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
142 |
val proof_stateN: string val proof_state: int -> T |
50543 | 143 |
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
|
144 |
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
|
145 |
val taskN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
146 |
val acceptedN: string val accepted: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
147 |
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
|
148 |
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
|
149 |
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
|
150 |
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
|
151 |
val failedN: string val failed: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
152 |
val serialN: string |
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
153 |
val serial_properties: int -> Properties.T |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50845
diff
changeset
|
154 |
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
|
155 |
val initN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
156 |
val statusN: string |
50503
50f141b34bb7
enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents:
50500
diff
changeset
|
157 |
val resultN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
158 |
val writelnN: string |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59125
diff
changeset
|
159 |
val stateN: string |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59125
diff
changeset
|
160 |
val informationN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
161 |
val tracingN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
162 |
val warningN: string |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
163 |
val legacyN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
164 |
val errorN: string |
57975
c657c68a60ab
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
wenzelm
parents:
57594
diff
changeset
|
165 |
val systemN: string |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
166 |
val protocolN: string |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
167 |
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
|
168 |
val no_reportN: string val no_report: T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
169 |
val badN: string val bad: T |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
170 |
val intensifyN: string val intensify: T |
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50683
diff
changeset
|
171 |
val browserN: string |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
172 |
val graphviewN: string |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
173 |
val sendbackN: string |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
174 |
val paddingN: string |
50842 | 175 |
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
|
176 |
val padding_command: Properties.entry |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
177 |
val dialogN: string val dialog: serial -> string -> T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
178 |
val functionN: string |
52563 | 179 |
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
|
180 |
val removed_versions: Properties.T |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51990
diff
changeset
|
181 |
val protocol_handler: string -> Properties.T |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
182 |
val invoke_scala: string -> string -> Properties.T |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
183 |
val cancel_scala: string -> Properties.T |
50842 | 184 |
val ML_statistics: Properties.entry |
50975 | 185 |
val task_statistics: Properties.entry |
51216 | 186 |
val command_timing: Properties.entry |
50845 | 187 |
val loading_theory: string -> Properties.T |
188 |
val dest_loading_theory: Properties.T -> string option |
|
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
189 |
val use_theories_result: string -> bool -> Properties.T |
56864 | 190 |
val print_operationsN: string |
191 |
val print_operations: Properties.T |
|
57594
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
56864
diff
changeset
|
192 |
val simp_trace_panelN: string |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
193 |
val simp_trace_logN: string |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
194 |
val simp_trace_stepN: string |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
195 |
val simp_trace_recurseN: string |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
196 |
val simp_trace_hintN: string |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
197 |
val simp_trace_ignoreN: string |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
198 |
val simp_trace_cancel: serial -> Properties.T |
40131
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
199 |
val no_output: Output.output * Output.output |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
200 |
val default_output: T -> Output.output * Output.output |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
201 |
val add_mode: string -> (T -> Output.output * Output.output) -> unit |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
202 |
val output: T -> Output.output * Output.output |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset
|
203 |
val enclose: T -> Output.output -> Output.output |
25552 | 204 |
val markup: T -> string -> string |
59125 | 205 |
val markups: T list -> string -> string |
43665 | 206 |
val markup_only: T -> string |
55956
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55919
diff
changeset
|
207 |
val markup_report: string -> string |
23623 | 208 |
end; |
209 |
||
210 |
structure Markup: MARKUP = |
|
211 |
struct |
|
212 |
||
30221 | 213 |
(** markup elements **) |
214 |
||
51988 | 215 |
(* misc values *) |
51951
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51665
diff
changeset
|
216 |
|
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51665
diff
changeset
|
217 |
fun parse_bool "true" = true |
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51665
diff
changeset
|
218 |
| parse_bool "false" = false |
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51665
diff
changeset
|
219 |
| parse_bool s = raise Fail ("Bad boolean: " ^ quote s); |
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51665
diff
changeset
|
220 |
|
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51665
diff
changeset
|
221 |
val print_bool = Bool.toString; |
fab4ab92e812
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents:
51665
diff
changeset
|
222 |
|
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
223 |
fun parse_int s = |
43797
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
224 |
let val i = Int.fromString s in |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
225 |
if is_none i orelse String.isPrefix "~" s |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
226 |
then raise Fail ("Bad integer: " ^ quote s) |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
227 |
else the i |
fad7758421bf
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents:
43748
diff
changeset
|
228 |
end; |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
229 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
230 |
val print_int = signed_string_of_int; |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
231 |
|
51988 | 232 |
fun parse_real s = |
233 |
(case Real.fromString s of |
|
234 |
SOME x => x |
|
235 |
| NONE => raise Fail ("Bad real: " ^ quote s)); |
|
236 |
||
51990 | 237 |
fun print_real x = |
238 |
let val s = signed_string_of_real x in |
|
239 |
(case space_explode "." s of |
|
240 |
[a, b] => if forall_string (fn c => c = "0") b then a else s |
|
241 |
| _ => s) |
|
242 |
end; |
|
51988 | 243 |
|
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset
|
244 |
|
23658 | 245 |
(* basic markup *) |
23623 | 246 |
|
28017 | 247 |
type T = string * Properties.T; |
23637 | 248 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
249 |
val empty = ("", []); |
23637 | 250 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
251 |
fun is_empty ("", _) = true |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
252 |
| is_empty _ = false; |
27883 | 253 |
|
23794 | 254 |
|
23671 | 255 |
fun properties more_props ((elem, props): T) = |
28017 | 256 |
(elem, fold_rev Properties.put more_props props); |
23671 | 257 |
|
55551 | 258 |
fun markup_elem name = (name, (name, []): T); |
259 |
fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T); |
|
260 |
fun markup_int name prop = (name, fn i => (name, [(prop, 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
|
261 |
|
26977 | 262 |
|
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
263 |
(* misc properties *) |
26977 | 264 |
|
23658 | 265 |
val nameN = "name"; |
27818 | 266 |
fun name a = properties [(nameN, a)]; |
267 |
||
23658 | 268 |
val kindN = "kind"; |
23671 | 269 |
|
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
270 |
val instanceN = "instance"; |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
271 |
|
23658 | 272 |
|
55550 | 273 |
(* embedded languages *) |
274 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
275 |
val languageN = "language"; |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55613
diff
changeset
|
276 |
val symbolsN = "symbols"; |
55666 | 277 |
val antiquotesN = "antiquotes"; |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
278 |
val delimitedN = "delimited" |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
279 |
|
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
280 |
fun is_delimited props = |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
281 |
Properties.get props delimitedN = SOME "true"; |
55666 | 282 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
283 |
fun language {name, symbols, antiquotes, delimited} = |
55666 | 284 |
(languageN, |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
285 |
[(nameN, name), |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
286 |
(symbolsN, print_bool symbols), |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
287 |
(antiquotesN, print_bool antiquotes), |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
288 |
(delimitedN, print_bool delimited)]); |
55550 | 289 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
290 |
fun language' {name, symbols, antiquotes} delimited = |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
291 |
language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
292 |
|
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
293 |
val language_method = |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
294 |
language {name = "method", symbols = true, antiquotes = false, delimited = false}; |
56033 | 295 |
val language_attribute = |
296 |
language {name = "attribute", symbols = true, antiquotes = false, delimited = false}; |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
297 |
val language_sort = language' {name = "sort", symbols = true, antiquotes = false}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
298 |
val language_type = language' {name = "type", symbols = true, antiquotes = false}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
299 |
val language_term = language' {name = "term", symbols = true, antiquotes = false}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
300 |
val language_prop = language' {name = "prop", symbols = true, antiquotes = false}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
301 |
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
|
302 |
val language_SML = language' {name = "SML", symbols = false, antiquotes = false}; |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
303 |
val language_document = language' {name = "document", symbols = false, antiquotes = true}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
304 |
val language_antiquotation = |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
305 |
language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
306 |
val language_text = language' {name = "text", symbols = true, antiquotes = false}; |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
307 |
val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true}; |
56034
1c59b555ac4a
some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
wenzelm
parents:
56033
diff
changeset
|
308 |
val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true}; |
55550 | 309 |
|
310 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
311 |
(* formal entities *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
312 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
313 |
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
|
314 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
315 |
val entityN = "entity"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
316 |
fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]); |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
317 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
318 |
fun get_entity_kind (name, props) = |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
319 |
if name = entityN then AList.lookup (op =) props kindN |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
320 |
else NONE; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
321 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
322 |
val defN = "def"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
323 |
val refN = "ref"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
324 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
325 |
|
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
326 |
(* completion *) |
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
327 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55687
diff
changeset
|
328 |
val (completionN, completion) = markup_elem "completion"; |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55837
diff
changeset
|
329 |
val (no_completionN, no_completion) = markup_elem "no_completion"; |
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
330 |
|
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
331 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
332 |
(* position *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
333 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
334 |
val lineN = "line"; |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58855
diff
changeset
|
335 |
val end_lineN = "end_line"; |
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58855
diff
changeset
|
336 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
337 |
val offsetN = "offset"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
338 |
val end_offsetN = "end_offset"; |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58855
diff
changeset
|
339 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
340 |
val fileN = "file"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
341 |
val idN = "id"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
342 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
343 |
val position_properties' = [fileN, idN]; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
344 |
val position_properties = [lineN, offsetN, end_offsetN] @ position_properties'; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
345 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
346 |
val (positionN, position) = markup_elem "position"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
347 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
348 |
|
58464 | 349 |
(* expression *) |
350 |
||
351 |
val (expressionN, expression) = markup_elem "expression"; |
|
352 |
||
353 |
||
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
354 |
(* citation *) |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
355 |
|
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
356 |
val (citationN, citation) = markup_string "citation" nameN; |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
357 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
358 |
|
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
359 |
(* external resources *) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
360 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
361 |
val (pathN, path) = markup_string "path" nameN; |
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
362 |
val (urlN, url) = markup_string "url" nameN; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
363 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
364 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
365 |
(* pretty printing *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
366 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
367 |
val indentN = "indent"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
368 |
val (blockN, block) = markup_int "block" indentN; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
369 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
370 |
val widthN = "width"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
371 |
val (breakN, break) = markup_int "break" widthN; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
372 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
373 |
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
|
374 |
|
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
|
375 |
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
|
376 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
377 |
|
56548 | 378 |
(* text properties *) |
379 |
||
380 |
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
|
381 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
382 |
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
|
383 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
384 |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57975
diff
changeset
|
385 |
(* misc entities *) |
56465 | 386 |
|
387 |
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
|
388 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
389 |
val theoryN = "theory"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
390 |
val classN = "class"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
391 |
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
|
392 |
val constantN = "constant"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
393 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
394 |
val (fixedN, fixed) = markup_string "fixed" nameN; |
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53055
diff
changeset
|
395 |
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
|
396 |
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
397 |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57975
diff
changeset
|
398 |
val method_modifierN = "method_modifier"; |
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57975
diff
changeset
|
399 |
|
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 |
(* inner syntax *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
402 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
403 |
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
|
404 |
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
|
405 |
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
|
406 |
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
|
407 |
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
|
408 |
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
|
409 |
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
|
410 |
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
|
411 |
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
|
412 |
val (inner_stringN, inner_string) = markup_elem "inner_string"; |
55033 | 413 |
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
|
414 |
val (inner_commentN, inner_comment) = markup_elem "inner_comment"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
415 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
416 |
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
|
417 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
418 |
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
|
419 |
val (typingN, typing) = markup_elem "typing"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
420 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
421 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
422 |
(* ML syntax *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
423 |
|
55505 | 424 |
val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1"; |
425 |
val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2"; |
|
426 |
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
|
427 |
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
|
428 |
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
|
429 |
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
|
430 |
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
|
431 |
val (ML_stringN, ML_string) = markup_elem "ML_string"; |
59112 | 432 |
val (ML_cartoucheN, ML_cartouche) = markup_elem "ML_cartouche"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
433 |
val (ML_commentN, ML_comment) = markup_elem "ML_comment"; |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
434 |
val (SML_stringN, SML_string) = markup_elem "SML_string"; |
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
435 |
val (SML_commentN, SML_comment) = markup_elem "SML_comment"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
436 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
437 |
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
|
438 |
val ML_openN = "ML_open"; |
55837 | 439 |
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
|
440 |
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
|
441 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
442 |
|
55550 | 443 |
(* antiquotations *) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
444 |
|
55526 | 445 |
val (antiquotedN, antiquoted) = markup_elem "antiquoted"; |
446 |
val (antiquoteN, antiquote) = markup_elem "antiquote"; |
|
447 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
448 |
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
|
449 |
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
|
450 |
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
|
451 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
452 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
453 |
(* text structure *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
454 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
455 |
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
|
456 |
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
|
457 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
458 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
459 |
(* outer syntax *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
460 |
|
55750
baa7a1e57f4a
back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;
wenzelm
parents:
55744
diff
changeset
|
461 |
val (commandN, command) = markup_elem "command"; |
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
462 |
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
|
463 |
val (keyword2N, keyword2) = markup_elem "keyword2"; |
55763 | 464 |
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
|
465 |
val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword"; |
56202 | 466 |
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
|
467 |
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
|
468 |
val (stringN, string) = markup_elem "string"; |
59081 | 469 |
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
|
470 |
val (verbatimN, verbatim) = markup_elem "verbatim"; |
55033 | 471 |
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
|
472 |
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
|
473 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
474 |
val tokenN = "token"; |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55763
diff
changeset
|
475 |
fun token delimited props = (tokenN, (delimitedN, print_bool delimited) :: props); |
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 |
(* timing *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
479 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
480 |
val elapsedN = "elapsed"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
481 |
val cpuN = "cpu"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
482 |
val gcN = "gc"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
483 |
|
50781 | 484 |
fun timing_properties {elapsed, cpu, gc} = |
485 |
[(elapsedN, Time.toString elapsed), |
|
486 |
(cpuN, Time.toString cpu), |
|
487 |
(gcN, Time.toString gc)]; |
|
488 |
||
51665 | 489 |
fun parse_timing_properties props = |
490 |
{elapsed = Properties.seconds props elapsedN, |
|
491 |
cpu = Properties.seconds props cpuN, |
|
492 |
gc = Properties.seconds props gcN}; |
|
51218
6425a0d3b7ac
support for build passing timings from Scala to ML;
wenzelm
parents:
51217
diff
changeset
|
493 |
|
51665 | 494 |
val timingN = "timing"; |
495 |
fun timing t = (timingN, timing_properties t); |
|
51218
6425a0d3b7ac
support for build passing timings from Scala to ML;
wenzelm
parents:
51217
diff
changeset
|
496 |
|
51228 | 497 |
|
498 |
(* command timing *) |
|
499 |
||
500 |
val command_timingN = "command_timing"; |
|
501 |
||
502 |
fun command_timing_properties {file, offset, name} elapsed = |
|
503 |
[(fileN, file), (offsetN, print_int offset), |
|
504 |
(nameN, name), (elapsedN, Time.toString elapsed)]; |
|
505 |
||
506 |
fun parse_command_timing_properties props = |
|
507 |
(case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of |
|
508 |
(SOME file, SOME offset, SOME name) => |
|
51665 | 509 |
SOME ({file = file, offset = parse_int offset, name = name}, |
510 |
Properties.seconds props elapsedN) |
|
51228 | 511 |
| _ => NONE); |
512 |
||
513 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
514 |
(* toplevel *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
515 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
516 |
val subgoalsN = "subgoals"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
517 |
val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
518 |
|
50543 | 519 |
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
|
520 |
val (subgoalN, subgoal) = markup_string "subgoal" nameN; |
50215 | 521 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50255
diff
changeset
|
522 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
523 |
(* command status *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
524 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
525 |
val taskN = "task"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
526 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
527 |
val (acceptedN, accepted) = markup_elem "accepted"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
528 |
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
|
529 |
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
|
530 |
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
|
531 |
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
|
532 |
val (failedN, failed) = markup_elem "failed"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
533 |
|
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 |
(* messages *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
536 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
537 |
val serialN = "serial"; |
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
538 |
fun serial_properties i = [(serialN, print_int i)]; |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
539 |
|
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50845
diff
changeset
|
540 |
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
|
541 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
542 |
val initN = "init"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
543 |
val statusN = "status"; |
50503
50f141b34bb7
enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents:
50500
diff
changeset
|
544 |
val resultN = "result"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
545 |
val writelnN = "writeln"; |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59125
diff
changeset
|
546 |
val stateN = "state" |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59125
diff
changeset
|
547 |
val informationN = "information"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
548 |
val tracingN = "tracing"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
549 |
val warningN = "warning"; |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
550 |
val legacyN = "legacy"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
551 |
val errorN = "error"; |
57975
c657c68a60ab
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
wenzelm
parents:
57594
diff
changeset
|
552 |
val systemN = "system"; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
553 |
val protocolN = "protocol"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
554 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
555 |
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
|
556 |
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
|
557 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
558 |
val (badN, bad) = markup_elem "bad"; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
559 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
560 |
val (intensifyN, intensify) = markup_elem "intensify"; |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
561 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
562 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
563 |
(* active areas *) |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
564 |
|
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50683
diff
changeset
|
565 |
val browserN = "browser" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
566 |
val graphviewN = "graphview"; |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
567 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
568 |
val sendbackN = "sendback"; |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
569 |
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
|
570 |
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
|
571 |
val padding_command = (paddingN, "command"); |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
572 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
573 |
val dialogN = "dialog"; |
50503
50f141b34bb7
enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents:
50500
diff
changeset
|
574 |
fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]); |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
575 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
576 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
577 |
(* protocol message functions *) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
578 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
579 |
val functionN = "function" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
580 |
|
52563 | 581 |
val assign_update = [(functionN, "assign_update")]; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
582 |
val removed_versions = [(functionN, "removed_versions")]; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
583 |
|
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51990
diff
changeset
|
584 |
fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)]; |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51990
diff
changeset
|
585 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
586 |
fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
587 |
fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
588 |
|
50683 | 589 |
val ML_statistics = (functionN, "ML_statistics"); |
50255 | 590 |
|
50975 | 591 |
val task_statistics = (functionN, "task_statistics"); |
592 |
||
51216 | 593 |
val command_timing = (functionN, "command_timing"); |
594 |
||
50845 | 595 |
fun loading_theory name = [("function", "loading_theory"), ("name", name)]; |
596 |
||
597 |
fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name |
|
598 |
| dest_loading_theory _ = NONE; |
|
599 |
||
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
600 |
fun use_theories_result id ok = |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
601 |
[("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)]; |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
602 |
|
56864 | 603 |
val print_operationsN = "print_operations"; |
604 |
val print_operations = [(functionN, print_operationsN)]; |
|
605 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
46894
diff
changeset
|
606 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
607 |
(* simplifier trace *) |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
608 |
|
57594
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
56864
diff
changeset
|
609 |
val simp_trace_panelN = "simp_trace_panel"; |
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
56864
diff
changeset
|
610 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
611 |
val simp_trace_logN = "simp_trace_log"; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
612 |
val simp_trace_stepN = "simp_trace_step"; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
613 |
val simp_trace_recurseN = "simp_trace_recurse"; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
614 |
val simp_trace_hintN = "simp_trace_hint"; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
615 |
val simp_trace_ignoreN = "simp_trace_ignore"; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
616 |
|
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
617 |
fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)]; |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
618 |
|
27969 | 619 |
|
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
620 |
|
30221 | 621 |
(** print mode operations **) |
23704 | 622 |
|
29325 | 623 |
val no_output = ("", ""); |
624 |
fun default_output (_: T) = no_output; |
|
23704 | 625 |
|
626 |
local |
|
627 |
val default = {output = default_output}; |
|
43684 | 628 |
val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]); |
23704 | 629 |
in |
43684 | 630 |
fun add_mode name output = |
46894
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45674
diff
changeset
|
631 |
Synchronized.change modes (fn tab => |
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45674
diff
changeset
|
632 |
(if not (Symtab.defined tab name) then () |
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45674
diff
changeset
|
633 |
else warning ("Redefining markup mode " ^ quote name); |
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45674
diff
changeset
|
634 |
Symtab.update (name, {output = output}) tab)); |
23704 | 635 |
fun get_mode () = |
43684 | 636 |
the_default default |
637 |
(Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); |
|
23623 | 638 |
end; |
23704 | 639 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
640 |
fun output m = if is_empty m then no_output else #output (get_mode ()) m; |
23704 | 641 |
|
23719 | 642 |
val enclose = output #-> Library.enclose; |
643 |
||
25552 | 644 |
fun markup m = |
645 |
let val (bg, en) = output m |
|
646 |
in Library.enclose (Output.escape bg) (Output.escape en) end; |
|
647 |
||
59125 | 648 |
val markups = fold_rev markup; |
649 |
||
43665 | 650 |
fun markup_only m = markup m ""; |
651 |
||
55956
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55919
diff
changeset
|
652 |
fun markup_report "" = "" |
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55919
diff
changeset
|
653 |
| markup_report txt = markup report txt; |
94d384d621b0
reject internal term names outright, and complete consts instead;
wenzelm
parents:
55919
diff
changeset
|
654 |
|
23704 | 655 |
end; |