author  wenzelm 
Tue, 05 Jul 2011 22:39:15 +0200  
changeset 43673  29eb1cd29961 
parent 43665  573d1272f36d 
child 43684  85388f5570c4 
permissions  rwrr 
23623  1 
(* Title: Pure/General/markup.ML 
2 
Author: Makarius 

3 

4 
Common markup elements. 

5 
*) 

6 

7 
signature MARKUP = 

8 
sig 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

9 
val parse_int: string > int 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

10 
val print_int: int > string 
28017  11 
type T = string * Properties.T 
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

12 
val empty: T 
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

13 
val is_empty: T > bool 
38229  14 
val properties: Properties.T > T > T 
23623  15 
val nameN: string 
27818  16 
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

17 
val kindN: string 
43547
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup  Binding.str_of is rendered obsolete;
wenzelm
parents:
43432
diff
changeset

18 
val bindingN: string val binding: T 
42135  19 
val entityN: string val entity: string > string > T 
43548
f231a7594e54
type classes: entity markup instead of oldstyle token markup;
wenzelm
parents:
43547
diff
changeset

20 
val get_entity_kind: T > string option 
33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32738
diff
changeset

21 
val defN: string 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32738
diff
changeset

22 
val refN: string 
23671  23 
val lineN: string 
26001  24 
val columnN: string 
27794  25 
val offsetN: string 
26 
val end_offsetN: string 

23671  27 
val fileN: string 
30221  28 
val idN: string 
27748  29 
val position_properties': string list 
26051  30 
val position_properties: string list 
23671  31 
val positionN: string val position: T 
43593  32 
val pathN: string val path: string > T 
23644  33 
val indentN: string 
23704  34 
val blockN: string val block: int > T 
23695  35 
val widthN: string 
23644  36 
val breakN: string val break: int > T 
37 
val fbreakN: string val fbreak: T 

33985  38 
val hiddenN: string val hidden: T 
43548
f231a7594e54
type classes: entity markup instead of oldstyle token markup;
wenzelm
parents:
43547
diff
changeset

39 
val classN: string 
43552  40 
val typeN: string 
41 
val constantN: string 

26702
a079f8f0080b
added markup for fixed variables (local constants);
wenzelm
parents:
26255
diff
changeset

42 
val fixedN: string val fixed: string > T 
27740  43 
val dynamic_factN: string val dynamic_fact: string > T 
23719  44 
val tfreeN: string val tfree: T 
45 
val tvarN: string val tvar: T 

46 
val freeN: string val free: T 

47 
val skolemN: string val skolem: T 

48 
val boundN: string val bound: T 

49 
val varN: string val var: T 

29318
6337d1cb2ba0
added numeral, which supercedes num, xnum, float;
wenzelm
parents:
28904
diff
changeset

50 
val numeralN: string val numeral: T 
27804  51 
val literalN: string val literal: T 
43432
224006e5ac46
inner literal/delimiter corresponds to outer keyword/operator;
wenzelm
parents:
42492
diff
changeset

52 
val delimiterN: string val delimiter: T 
29318
6337d1cb2ba0
added numeral, which supercedes num, xnum, float;
wenzelm
parents:
28904
diff
changeset

53 
val inner_stringN: string val inner_string: T 
27883  54 
val inner_commentN: string val inner_comment: T 
39168
e3ac771235f7
report token range after inner parse error  often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38887
diff
changeset

55 
val token_rangeN: string val token_range: T 
23637  56 
val sortN: string val sort: T 
57 
val typN: string val typ: T 

58 
val termN: string val term: T 

27818  59 
val propN: string val prop: T 
30614  60 
val ML_keywordN: string val ML_keyword: T 
37195  61 
val ML_delimiterN: string val ML_delimiter: T 
30614  62 
val ML_identN: string val ML_ident: T 
63 
val ML_tvarN: string val ML_tvar: T 

64 
val ML_numeralN: string val ML_numeral: T 

65 
val ML_charN: string val ML_char: T 

66 
val ML_stringN: string val ML_string: T 

67 
val ML_commentN: string val ML_comment: T 

68 
val ML_malformedN: string val ML_malformed: T 

42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42135
diff
changeset

69 
val ML_defN: string 
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42135
diff
changeset

70 
val ML_openN: string 
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42135
diff
changeset

71 
val ML_structN: string 
30702  72 
val ML_typingN: string val ML_typing: T 
27875  73 
val ML_sourceN: string val ML_source: T 
74 
val doc_sourceN: string val doc_source: T 

27879  75 
val antiqN: string val antiq: T 
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43552
diff
changeset

76 
val ML_antiquotationN: string 
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43560
diff
changeset

77 
val doc_antiquotationN: string 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43560
diff
changeset

78 
val doc_antiquotation_optionN: string 
27836  79 
val keyword_declN: string val keyword_decl: string > T 
80 
val command_declN: string val command_decl: string > string > T 

37193  81 
val keywordN: string val keyword: T 
37192  82 
val operatorN: string val operator: T 
37193  83 
val commandN: string val command: T 
27836  84 
val identN: string val ident: T 
23719  85 
val stringN: string val string: T 
86 
val altstringN: string val altstring: T 

87 
val verbatimN: string val verbatim: T 

88 
val commentN: string val comment: T 

89 
val controlN: string val control: T 

90 
val malformedN: string val malformed: T 

38229  91 
val tokenN: string val token: Properties.T > T 
27660  92 
val command_spanN: string val command_span: string > T 
93 
val ignored_spanN: string val ignored_span: T 

27836  94 
val malformed_spanN: string val malformed_span: T 
43673
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43665
diff
changeset

95 
val loaded_theoryN: string val loaded_theory: string > T 
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

96 
val elapsedN: string 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

97 
val cpuN: string 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

98 
val gcN: string 
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41484
diff
changeset

99 
val timingN: string val timing: Timing.timing > T 
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

100 
val subgoalsN: string 
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

101 
val proof_stateN: string val proof_state: int > T 
23637  102 
val stateN: string val state: T 
103 
val subgoalN: string val subgoal: T 

24289  104 
val sendbackN: string val sendback: T 
24555  105 
val hiliteN: string val hilite: T 
29417  106 
val taskN: string 
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
34242
diff
changeset

107 
val forkedN: string val forked: T 
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
34242
diff
changeset

108 
val joinedN: string val joined: T 
27615  109 
val failedN: string val failed: T 
27606  110 
val finishedN: string val finished: T 
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

111 
val versionN: string 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

112 
val execN: string 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

113 
val assignN: string val assign: int > T 
43665  114 
val editN: string val edit: int * int > T 
38871  115 
val serialN: string 
27969  116 
val promptN: string val prompt: T 
31384
ce169bd37fc0
IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents:
30702
diff
changeset

117 
val readyN: string val ready: 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

118 
val reportN: string val report: T 
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39171
diff
changeset

119 
val no_reportN: string val no_report: T 
39171
525a13b9ac74
highlight bad range of nested error (here from inner parsing);
wenzelm
parents:
39168
diff
changeset

120 
val badN: string val bad: T 
40131
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
39585
diff
changeset

121 
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

122 
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

123 
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

124 
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

125 
val enclose: T > Output.output > Output.output 
25552  126 
val markup: T > string > string 
43665  127 
val markup_only: T > string 
23623  128 
end; 
129 

130 
structure Markup: MARKUP = 

131 
struct 

132 

30221  133 
(** markup elements **) 
134 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

135 
(* integers *) 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

136 

49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

137 
fun parse_int s = 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

138 
(case Int.fromString s of 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

139 
SOME i => i 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

140 
 NONE => raise Fail ("Bad integer: " ^ quote s)); 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

141 

49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

142 
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

143 

49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

144 

23658  145 
(* basic markup *) 
23623  146 

28017  147 
type T = string * Properties.T; 
23637  148 

38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

149 
val empty = ("", []); 
23637  150 

38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

151 
fun is_empty ("", _) = true 
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

152 
 is_empty _ = false; 
27883  153 

23794  154 

23671  155 
fun properties more_props ((elem, props): T) = 
28017  156 
(elem, fold_rev Properties.put more_props props); 
23671  157 

25552  158 
fun markup_elem elem = (elem, (elem, []): T); 
23794  159 
fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T); 
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

160 
fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T); 
23794  161 

26977  162 

38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

163 
(* misc properties *) 
26977  164 

23658  165 
val nameN = "name"; 
27818  166 
fun name a = properties [(nameN, a)]; 
167 

23658  168 
val kindN = "kind"; 
23671  169 

23658  170 

33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32738
diff
changeset

171 
(* formal entities *) 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32738
diff
changeset

172 

43547
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup  Binding.str_of is rendered obsolete;
wenzelm
parents:
43432
diff
changeset

173 
val (bindingN, binding) = markup_elem "binding"; 
42135  174 

175 
val entityN = "entity"; 

42377  176 
fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]); 
33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32738
diff
changeset

177 

43548
f231a7594e54
type classes: entity markup instead of oldstyle token markup;
wenzelm
parents:
43547
diff
changeset

178 
fun get_entity_kind (name, props) = 
f231a7594e54
type classes: entity markup instead of oldstyle token markup;
wenzelm
parents:
43547
diff
changeset

179 
if name = entityN then AList.lookup (op =) props kindN 
f231a7594e54
type classes: entity markup instead of oldstyle token markup;
wenzelm
parents:
43547
diff
changeset

180 
else NONE; 
f231a7594e54
type classes: entity markup instead of oldstyle token markup;
wenzelm
parents:
43547
diff
changeset

181 

33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32738
diff
changeset

182 
val defN = "def"; 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32738
diff
changeset

183 
val refN = "ref"; 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32738
diff
changeset

184 

757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32738
diff
changeset

185 

23671  186 
(* position *) 
187 

188 
val lineN = "line"; 

26001  189 
val columnN = "column"; 
27794  190 
val offsetN = "offset"; 
191 
val end_offsetN = "end_offset"; 

23671  192 
val fileN = "file"; 
25816  193 
val idN = "id"; 
23671  194 

41484  195 
val position_properties' = [fileN, idN]; 
196 
val position_properties = [lineN, columnN, offsetN, end_offsetN] @ position_properties'; 

27748  197 

25552  198 
val (positionN, position) = markup_elem "position"; 
26255  199 

23644  200 

43593  201 
(* path *) 
202 

203 
val (pathN, path) = markup_string "path" nameN; 

204 

205 

23644  206 
(* pretty printing *) 
207 

208 
val indentN = "indent"; 

209 
val (blockN, block) = markup_int "block" indentN; 

210 

211 
val widthN = "width"; 

212 
val (breakN, break) = markup_int "break" widthN; 

213 

25552  214 
val (fbreakN, fbreak) = markup_elem "fbreak"; 
23637  215 

216 

33985  217 
(* hidden text *) 
218 

219 
val (hiddenN, hidden) = markup_elem "hidden"; 

220 

221 

23623  222 
(* logical entities *) 
223 

43548
f231a7594e54
type classes: entity markup instead of oldstyle token markup;
wenzelm
parents:
43547
diff
changeset

224 
val classN = "class"; 
43552  225 
val typeN = "type"; 
226 
val constantN = "constant"; 

227 

26702
a079f8f0080b
added markup for fixed variables (local constants);
wenzelm
parents:
26255
diff
changeset

228 
val (fixedN, fixed) = markup_string "fixed" nameN; 
27740  229 
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; 
23623  230 

231 

232 
(* inner syntax *) 

233 

25552  234 
val (tfreeN, tfree) = markup_elem "tfree"; 
235 
val (tvarN, tvar) = markup_elem "tvar"; 

236 
val (freeN, free) = markup_elem "free"; 

237 
val (skolemN, skolem) = markup_elem "skolem"; 

238 
val (boundN, bound) = markup_elem "bound"; 

239 
val (varN, var) = markup_elem "var"; 

29318
6337d1cb2ba0
added numeral, which supercedes num, xnum, float;
wenzelm
parents:
28904
diff
changeset

240 
val (numeralN, numeral) = markup_elem "numeral"; 
27804  241 
val (literalN, literal) = markup_elem "literal"; 
43432
224006e5ac46
inner literal/delimiter corresponds to outer keyword/operator;
wenzelm
parents:
42492
diff
changeset

242 
val (delimiterN, delimiter) = markup_elem "delimiter"; 
29318
6337d1cb2ba0
added numeral, which supercedes num, xnum, float;
wenzelm
parents:
28904
diff
changeset

243 
val (inner_stringN, inner_string) = markup_elem "inner_string"; 
27883  244 
val (inner_commentN, inner_comment) = markup_elem "inner_comment"; 
23719  245 

39168
e3ac771235f7
report token range after inner parse error  often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38887
diff
changeset

246 
val (token_rangeN, token_range) = markup_elem "token_range"; 
e3ac771235f7
report token range after inner parse error  often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38887
diff
changeset

247 

25552  248 
val (sortN, sort) = markup_elem "sort"; 
249 
val (typN, typ) = markup_elem "typ"; 

250 
val (termN, term) = markup_elem "term"; 

27818  251 
val (propN, prop) = markup_elem "prop"; 
27748  252 

23623  253 

30614  254 
(* ML syntax *) 
255 

256 
val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword"; 

37195  257 
val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter"; 
30614  258 
val (ML_identN, ML_ident) = markup_elem "ML_ident"; 
259 
val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar"; 

260 
val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral"; 

261 
val (ML_charN, ML_char) = markup_elem "ML_char"; 

262 
val (ML_stringN, ML_string) = markup_elem "ML_string"; 

263 
val (ML_commentN, ML_comment) = markup_elem "ML_comment"; 

264 
val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed"; 

265 

42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42135
diff
changeset

266 
val ML_defN = "ML_def"; 
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42135
diff
changeset

267 
val ML_openN = "ML_open"; 
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42135
diff
changeset

268 
val ML_structN = "ML_struct"; 
30702  269 
val (ML_typingN, ML_typing) = markup_elem "ML_typing"; 
270 

30614  271 

27875  272 
(* embedded source text *) 
273 

274 
val (ML_sourceN, ML_source) = markup_elem "ML_source"; 

275 
val (doc_sourceN, doc_source) = markup_elem "doc_source"; 

276 

27879  277 
val (antiqN, antiq) = markup_elem "antiq"; 
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43552
diff
changeset

278 
val ML_antiquotationN = "ML antiquotation"; 
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43560
diff
changeset

279 
val doc_antiquotationN = "document antiquotation"; 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43560
diff
changeset

280 
val doc_antiquotation_optionN = "document antiquotation option"; 
27879  281 

27875  282 

23623  283 
(* outer syntax *) 
284 

24870  285 
val (keyword_declN, keyword_decl) = markup_string "keyword_decl" nameN; 
286 

287 
val command_declN = "command_decl"; 

288 
fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]); 

289 

37193  290 
val (keywordN, keyword) = markup_elem "keyword"; 
37192  291 
val (operatorN, operator) = markup_elem "operator"; 
37193  292 
val (commandN, command) = markup_elem "command"; 
27836  293 
val (identN, ident) = markup_elem "ident"; 
25552  294 
val (stringN, string) = markup_elem "string"; 
295 
val (altstringN, altstring) = markup_elem "altstring"; 

296 
val (verbatimN, verbatim) = markup_elem "verbatim"; 

297 
val (commentN, comment) = markup_elem "comment"; 

298 
val (controlN, control) = markup_elem "control"; 

299 
val (malformedN, malformed) = markup_elem "malformed"; 

23719  300 

38229  301 
val tokenN = "token"; 
302 
fun token props = (tokenN, props); 

27851  303 

27660  304 
val (command_spanN, command_span) = markup_string "command_span" nameN; 
305 
val (ignored_spanN, ignored_span) = markup_elem "ignored_span"; 

27836  306 
val (malformed_spanN, malformed_span) = markup_elem "malformed_span"; 
23719  307 

23623  308 

43673
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43665
diff
changeset

309 
(* theory loader *) 
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43665
diff
changeset

310 

29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43665
diff
changeset

311 
val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" nameN; 
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43665
diff
changeset

312 

29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43665
diff
changeset

313 

40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

314 
(* timing *) 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

315 

6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

316 
val timingN = "timing"; 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

317 
val elapsedN = "elapsed"; 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

318 
val cpuN = "cpu"; 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

319 
val gcN = "gc"; 
23637  320 

42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41484
diff
changeset

321 
fun timing {elapsed, cpu, gc} = 
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

322 
(timingN, 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

323 
[(elapsedN, Time.toString elapsed), 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

324 
(cpuN, Time.toString cpu), 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

325 
(gcN, Time.toString gc)]); 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

326 

6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

327 

6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40391
diff
changeset

328 
(* toplevel *) 
40391
b0dafbfc05b7
explicit "timing" status for toplevel transactions;
wenzelm
parents:
40131
diff
changeset

329 

38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

330 
val subgoalsN = "subgoals"; 
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

331 
val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN; 
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

332 

25552  333 
val (stateN, state) = markup_elem "state"; 
334 
val (subgoalN, subgoal) = markup_elem "subgoal"; 

335 
val (sendbackN, sendback) = markup_elem "sendback"; 

336 
val (hiliteN, hilite) = markup_elem "hilite"; 

337 

338 

27606  339 
(* command status *) 
340 

29417  341 
val taskN = "task"; 
342 

37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
34242
diff
changeset

343 
val (forkedN, forked) = markup_elem "forked"; 
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
34242
diff
changeset

344 
val (joinedN, joined) = markup_elem "joined"; 
38429
9951852fae91
simplified command status: interpret stacked markup on demand;
wenzelm
parents:
38414
diff
changeset

345 

27615  346 
val (failedN, failed) = markup_elem "failed"; 
27606  347 
val (finishedN, finished) = markup_elem "finished"; 
348 

29488  349 

350 
(* interactive documents *) 

351 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

352 
val versionN = "version"; 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

353 
val execN = "exec"; 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38229
diff
changeset

354 
val (assignN, assign) = markup_int "assign" versionN; 
34242
5ccdc8bf3849
explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
wenzelm
parents:
34214
diff
changeset

355 

29488  356 
val editN = "edit"; 
43665  357 
fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]); 
29482  358 

27606  359 

27969  360 
(* messages *) 
361 

38871  362 
val serialN = "serial"; 
27969  363 

364 
val (promptN, prompt) = markup_elem "prompt"; 

31384
ce169bd37fc0
IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents:
30702
diff
changeset

365 
val (readyN, ready) = markup_elem "ready"; 
27969  366 

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

367 
val (reportN, report) = markup_elem "report"; 
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39171
diff
changeset

368 
val (no_reportN, no_report) = markup_elem "no_report"; 
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

369 

39171
525a13b9ac74
highlight bad range of nested error (here from inner parsing);
wenzelm
parents:
39168
diff
changeset

370 
val (badN, bad) = markup_elem "bad"; 
525a13b9ac74
highlight bad range of nested error (here from inner parsing);
wenzelm
parents:
39168
diff
changeset

371 

27969  372 

373 

30221  374 
(** print mode operations **) 
23704  375 

29325  376 
val no_output = ("", ""); 
377 
fun default_output (_: T) = no_output; 

23704  378 

379 
local 

380 
val default = {output = default_output}; 

32738  381 
val modes = Unsynchronized.ref (Symtab.make [("", default)]); 
23704  382 
in 
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
23794
diff
changeset

383 
fun add_mode name output = CRITICAL (fn () => 
32738  384 
Unsynchronized.change modes (Symtab.update_new (name, {output = output}))); 
23704  385 
fun get_mode () = 
24612  386 
the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ())); 
23623  387 
end; 
23704  388 

38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

389 
fun output m = if is_empty m then no_output else #output (get_mode ()) m; 
23704  390 

23719  391 
val enclose = output #> Library.enclose; 
392 

25552  393 
fun markup m = 
394 
let val (bg, en) = output m 

395 
in Library.enclose (Output.escape bg) (Output.escape en) end; 

396 

43665  397 
fun markup_only m = markup m ""; 
398 

23704  399 
end; 