1(* Title: Pure/PIDE/markup.ML 2 Author: Makarius 3 4Quasi-abstract markup elements. 5*) 6 7signature MARKUP = 8sig 9 type T = string * Properties.T 10 val empty: T 11 val is_empty: T -> bool 12 val properties: Properties.T -> T -> T 13 val nameN: string 14 val name: string -> T -> T 15 val kindN: string 16 val serialN: string 17 val serial_properties: int -> Properties.T 18 val instanceN: string 19 val languageN: string 20 val symbolsN: string 21 val delimitedN: string 22 val is_delimited: Properties.T -> bool 23 val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T 24 val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T 25 val language_Isar: bool -> T 26 val language_method: T 27 val language_attribute: T 28 val language_sort: bool -> T 29 val language_type: bool -> T 30 val language_term: bool -> T 31 val language_prop: bool -> T 32 val language_ML: bool -> T 33 val language_SML: bool -> T 34 val language_document: bool -> T 35 val language_antiquotation: T 36 val language_text: bool -> T 37 val language_verbatim: bool -> T 38 val language_latex: bool -> T 39 val language_rail: T 40 val language_path: T 41 val language_mixfix: T 42 val bindingN: string val binding: T 43 val entityN: string val entity: string -> string -> T 44 val get_entity_kind: T -> string option 45 val defN: string 46 val refN: string 47 val completionN: string val completion: T 48 val no_completionN: string val no_completion: T 49 val lineN: string 50 val end_lineN: string 51 val offsetN: string 52 val end_offsetN: string 53 val fileN: string 54 val idN: string 55 val position_properties': string list 56 val position_properties: string list 57 val positionN: string val position: T 58 val expressionN: string val expression: string -> T 59 val citationN: string val citation: string -> T 60 val pathN: string val path: string -> T 61 val urlN: string val url: string -> T 62 val docN: string val doc: string -> T 63 val markupN: string 64 val consistentN: string 65 val unbreakableN: string 66 val block_properties: string list 67 val indentN: string 68 val widthN: string 69 val blockN: string val block: bool -> int -> T 70 val breakN: string val break: int -> int -> T 71 val fbreakN: string val fbreak: T 72 val itemN: string val item: T 73 val wordsN: string val words: T 74 val no_wordsN: string val no_words: T 75 val hiddenN: string val hidden: T 76 val deleteN: string val delete: T 77 val system_optionN: string 78 val sessionN: string 79 val theoryN: string 80 val classN: string 81 val type_nameN: string 82 val constantN: string 83 val fixedN: string val fixed: string -> T 84 val caseN: string val case_: string -> T 85 val dynamic_factN: string val dynamic_fact: string -> T 86 val literal_factN: string val literal_fact: string -> T 87 val method_modifierN: string 88 val tfreeN: string val tfree: T 89 val tvarN: string val tvar: T 90 val freeN: string val free: T 91 val skolemN: string val skolem: T 92 val boundN: string val bound: T 93 val varN: string val var: T 94 val numeralN: string val numeral: T 95 val literalN: string val literal: T 96 val delimiterN: string val delimiter: T 97 val inner_stringN: string val inner_string: T 98 val inner_cartoucheN: string val inner_cartouche: T 99 val inner_commentN: string val inner_comment: T 100 val token_rangeN: string val token_range: T 101 val sortingN: string val sorting: T 102 val typingN: string val typing: T 103 val class_parameterN: string val class_parameter: T 104 val ML_keyword1N: string val ML_keyword1: T 105 val ML_keyword2N: string val ML_keyword2: T 106 val ML_keyword3N: string val ML_keyword3: T 107 val ML_delimiterN: string val ML_delimiter: T 108 val ML_tvarN: string val ML_tvar: T 109 val ML_numeralN: string val ML_numeral: T 110 val ML_charN: string val ML_char: T 111 val ML_stringN: string val ML_string: T 112 val ML_commentN: string val ML_comment: T 113 val SML_stringN: string val SML_string: T 114 val SML_commentN: string val SML_comment: T 115 val ML_defN: string 116 val ML_openN: string 117 val ML_structureN: string 118 val ML_typingN: string val ML_typing: T 119 val ML_breakpointN: string val ML_breakpoint: int -> T 120 val antiquotedN: string val antiquoted: T 121 val antiquoteN: string val antiquote: T 122 val ML_antiquotationN: string 123 val document_antiquotationN: string 124 val document_antiquotation_optionN: string 125 val paragraphN: string val paragraph: T 126 val text_foldN: string val text_fold: T 127 val markdown_paragraphN: string val markdown_paragraph: T 128 val markdown_itemN: string val markdown_item: T 129 val markdown_bulletN: string val markdown_bullet: int -> T 130 val markdown_listN: string val markdown_list: string -> T 131 val itemizeN: string 132 val enumerateN: string 133 val descriptionN: string 134 val inputN: string val input: bool -> Properties.T -> T 135 val command_keywordN: string val command_keyword: T 136 val commandN: string val command_properties: T -> T 137 val keywordN: string val keyword_properties: T -> T 138 val stringN: string val string: T 139 val alt_stringN: string val alt_string: T 140 val verbatimN: string val verbatim: T 141 val cartoucheN: string val cartouche: T 142 val commentN: string val comment: T 143 val keyword1N: string val keyword1: T 144 val keyword2N: string val keyword2: T 145 val keyword3N: string val keyword3: T 146 val quasi_keywordN: string val quasi_keyword: T 147 val improperN: string val improper: T 148 val operatorN: string val operator: T 149 val elapsedN: string 150 val cpuN: string 151 val gcN: string 152 val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T 153 val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time} 154 val command_timingN: string 155 val command_timing_properties: 156 {file: string, offset: int, name: string} -> Time.time -> Properties.T 157 val parse_command_timing_properties: 158 Properties.T -> ({file: string, offset: int, name: string} * Time.time) option 159 val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T 160 val command_indentN: string val command_indent: int -> T 161 val goalN: string val goal: T 162 val subgoalN: string val subgoal: string -> T 163 val taskN: string 164 val acceptedN: string val accepted: T 165 val forkedN: string val forked: T 166 val joinedN: string val joined: T 167 val runningN: string val running: T 168 val finishedN: string val finished: T 169 val failedN: string val failed: T 170 val initializedN: string val initialized: T 171 val consolidatedN: string val consolidated: T 172 val exec_idN: string 173 val initN: string 174 val statusN: string val status: T 175 val resultN: string val result: T 176 val writelnN: string val writeln: T 177 val stateN: string val state: T 178 val informationN: string val information: T 179 val tracingN: string val tracing: T 180 val warningN: string val warning: T 181 val legacyN: string val legacy: T 182 val errorN: string val error: T 183 val systemN: string val system: T 184 val protocolN: string 185 val reportN: string val report: T 186 val no_reportN: string val no_report: T 187 val badN: string val bad: unit -> T 188 val intensifyN: string val intensify: T 189 val browserN: string 190 val graphviewN: string 191 val sendbackN: string 192 val paddingN: string 193 val padding_line: Properties.entry 194 val padding_command: Properties.entry 195 val dialogN: string val dialog: serial -> string -> T 196 val jedit_actionN: string 197 val functionN: string 198 val assign_update: Properties.T 199 val removed_versions: Properties.T 200 val protocol_handler: string -> Properties.T 201 val invoke_scala: string -> string -> Properties.T 202 val cancel_scala: string -> Properties.T 203 val ML_statistics: Properties.entry 204 val task_statistics: Properties.entry 205 val command_timing: Properties.entry 206 val theory_timing: Properties.entry 207 val exportN: string 208 type export_args = 209 {id: string option, serial: serial, theory_name: string, name: string, compress: bool} 210 val export: export_args -> Properties.T 211 val loading_theory: string -> Properties.T 212 val dest_loading_theory: Properties.T -> string option 213 val build_session_finished: Properties.T 214 val print_operationsN: string 215 val print_operations: Properties.T 216 val debugger_state: string -> Properties.T 217 val debugger_output: string -> Properties.T 218 val simp_trace_panelN: string 219 val simp_trace_logN: string 220 val simp_trace_stepN: string 221 val simp_trace_recurseN: string 222 val simp_trace_hintN: string 223 val simp_trace_ignoreN: string 224 val simp_trace_cancel: serial -> Properties.T 225 val no_output: Output.output * Output.output 226 val add_mode: string -> (T -> Output.output * Output.output) -> unit 227 val output: T -> Output.output * Output.output 228 val enclose: T -> Output.output -> Output.output 229 val markup: T -> string -> string 230 val markups: T list -> string -> string 231 val markup_only: T -> string 232 val markup_report: string -> string 233end; 234 235structure Markup: MARKUP = 236struct 237 238(** markup elements **) 239 240(* basic markup *) 241 242type T = string * Properties.T; 243 244val empty = ("", []); 245 246fun is_empty ("", _) = true 247 | is_empty _ = false; 248 249 250fun properties more_props ((elem, props): T) = 251 (elem, fold_rev Properties.put more_props props); 252 253fun markup_elem name = (name, (name, []): T); 254fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T); 255fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T); 256 257 258(* misc properties *) 259 260val nameN = "name"; 261fun name a = properties [(nameN, a)]; 262 263val kindN = "kind"; 264 265val serialN = "serial"; 266fun serial_properties i = [(serialN, Value.print_int i)]; 267 268val instanceN = "instance"; 269 270 271(* embedded languages *) 272 273val languageN = "language"; 274val symbolsN = "symbols"; 275val antiquotesN = "antiquotes"; 276val delimitedN = "delimited" 277 278fun is_delimited props = 279 Properties.get props delimitedN = SOME "true"; 280 281fun language {name, symbols, antiquotes, delimited} = 282 (languageN, 283 [(nameN, name), 284 (symbolsN, Value.print_bool symbols), 285 (antiquotesN, Value.print_bool antiquotes), 286 (delimitedN, Value.print_bool delimited)]); 287 288fun language' {name, symbols, antiquotes} delimited = 289 language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited}; 290 291val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false}; 292val language_method = 293 language {name = "method", symbols = true, antiquotes = false, delimited = false}; 294val language_attribute = 295 language {name = "attribute", symbols = true, antiquotes = false, delimited = false}; 296val language_sort = language' {name = "sort", symbols = true, antiquotes = false}; 297val language_type = language' {name = "type", symbols = true, antiquotes = false}; 298val language_term = language' {name = "term", symbols = true, antiquotes = false}; 299val language_prop = language' {name = "prop", symbols = true, antiquotes = false}; 300val language_ML = language' {name = "ML", symbols = false, antiquotes = true}; 301val language_SML = language' {name = "SML", symbols = false, antiquotes = false}; 302val language_document = language' {name = "document", symbols = false, antiquotes = true}; 303val language_antiquotation = 304 language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; 305val language_text = language' {name = "text", symbols = true, antiquotes = false}; 306val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false}; 307val language_latex = language' {name = "latex", symbols = false, antiquotes = false}; 308val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true}; 309val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true}; 310val language_mixfix = 311 language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true}; 312 313 314(* formal entities *) 315 316val (bindingN, binding) = markup_elem "binding"; 317 318val entityN = "entity"; 319fun entity kind name = 320 (entityN, 321 (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)])); 322 323fun get_entity_kind (name, props) = 324 if name = entityN then Properties.get props kindN 325 else NONE; 326 327val defN = "def"; 328val refN = "ref"; 329 330 331(* completion *) 332 333val (completionN, completion) = markup_elem "completion"; 334val (no_completionN, no_completion) = markup_elem "no_completion"; 335 336 337(* position *) 338 339val lineN = "line"; 340val end_lineN = "end_line"; 341 342val offsetN = "offset"; 343val end_offsetN = "end_offset"; 344 345val fileN = "file"; 346val idN = "id"; 347 348val position_properties' = [fileN, idN]; 349val position_properties = [lineN, offsetN, end_offsetN] @ position_properties'; 350 351val (positionN, position) = markup_elem "position"; 352 353 354(* expression *) 355 356val expressionN = "expression"; 357fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]); 358 359 360(* citation *) 361 362val (citationN, citation) = markup_string "citation" nameN; 363 364 365(* external resources *) 366 367val (pathN, path) = markup_string "path" nameN; 368val (urlN, url) = markup_string "url" nameN; 369val (docN, doc) = markup_string "doc" nameN; 370 371 372(* pretty printing *) 373 374val markupN = "markup"; 375val consistentN = "consistent"; 376val unbreakableN = "unbreakable"; 377val indentN = "indent"; 378 379val block_properties = [markupN, consistentN, unbreakableN, indentN]; 380 381val widthN = "width"; 382 383val blockN = "block"; 384fun block c i = 385 (blockN, 386 (if c then [(consistentN, Value.print_bool c)] else []) @ 387 (if i <> 0 then [(indentN, Value.print_int i)] else [])); 388 389val breakN = "break"; 390fun break w i = 391 (breakN, 392 (if w <> 0 then [(widthN, Value.print_int w)] else []) @ 393 (if i <> 0 then [(indentN, Value.print_int i)] else [])); 394 395val (fbreakN, fbreak) = markup_elem "fbreak"; 396 397val (itemN, item) = markup_elem "item"; 398 399 400(* text properties *) 401 402val (wordsN, words) = markup_elem "words"; 403val (no_wordsN, no_words) = markup_elem "no_words"; 404 405val (hiddenN, hidden) = markup_elem "hidden"; 406 407val (deleteN, delete) = markup_elem "delete"; 408 409 410(* misc entities *) 411 412val system_optionN = "system_option"; 413 414val sessionN = "session"; 415 416val theoryN = "theory"; 417val classN = "class"; 418val type_nameN = "type_name"; 419val constantN = "constant"; 420 421val (fixedN, fixed) = markup_string "fixed" nameN; 422val (caseN, case_) = markup_string "case" nameN; 423val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; 424val (literal_factN, literal_fact) = markup_string "literal_fact" nameN; 425 426val method_modifierN = "method_modifier"; 427 428 429(* inner syntax *) 430 431val (tfreeN, tfree) = markup_elem "tfree"; 432val (tvarN, tvar) = markup_elem "tvar"; 433val (freeN, free) = markup_elem "free"; 434val (skolemN, skolem) = markup_elem "skolem"; 435val (boundN, bound) = markup_elem "bound"; 436val (varN, var) = markup_elem "var"; 437val (numeralN, numeral) = markup_elem "numeral"; 438val (literalN, literal) = markup_elem "literal"; 439val (delimiterN, delimiter) = markup_elem "delimiter"; 440val (inner_stringN, inner_string) = markup_elem "inner_string"; 441val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"; 442val (inner_commentN, inner_comment) = markup_elem "inner_comment"; 443 444val (token_rangeN, token_range) = markup_elem "token_range"; 445 446val (sortingN, sorting) = markup_elem "sorting"; 447val (typingN, typing) = markup_elem "typing"; 448val (class_parameterN, class_parameter) = markup_elem "class_parameter"; 449 450 451(* ML *) 452 453val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1"; 454val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2"; 455val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3"; 456val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter"; 457val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar"; 458val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral"; 459val (ML_charN, ML_char) = markup_elem "ML_char"; 460val (ML_stringN, ML_string) = markup_elem "ML_string"; 461val (ML_commentN, ML_comment) = markup_elem "ML_comment"; 462val (SML_stringN, SML_string) = markup_elem "SML_string"; 463val (SML_commentN, SML_comment) = markup_elem "SML_comment"; 464 465val ML_defN = "ML_def"; 466val ML_openN = "ML_open"; 467val ML_structureN = "ML_structure"; 468val (ML_typingN, ML_typing) = markup_elem "ML_typing"; 469 470val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN; 471 472 473(* antiquotations *) 474 475val (antiquotedN, antiquoted) = markup_elem "antiquoted"; 476val (antiquoteN, antiquote) = markup_elem "antiquote"; 477 478val ML_antiquotationN = "ML_antiquotation"; 479val document_antiquotationN = "document_antiquotation"; 480val document_antiquotation_optionN = "document_antiquotation_option"; 481 482 483(* text structure *) 484 485val (paragraphN, paragraph) = markup_elem "paragraph"; 486val (text_foldN, text_fold) = markup_elem "text_fold"; 487 488 489(* Markdown document structure *) 490 491val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph"; 492val (markdown_itemN, markdown_item) = markup_elem "markdown_item"; 493val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth"; 494val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN; 495 496val itemizeN = "itemize"; 497val enumerateN = "enumerate"; 498val descriptionN = "description"; 499 500 501(* formal input *) 502 503val inputN = "input"; 504fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props); 505 506 507(* outer syntax *) 508 509val (command_keywordN, command_keyword) = markup_elem "command_keyword"; 510 511val commandN = "command"; val command_properties = properties [(kindN, commandN)]; 512val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)]; 513 514val (keyword1N, keyword1) = markup_elem "keyword1"; 515val (keyword2N, keyword2) = markup_elem "keyword2"; 516val (keyword3N, keyword3) = markup_elem "keyword3"; 517val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword"; 518val (improperN, improper) = markup_elem "improper"; 519val (operatorN, operator) = markup_elem "operator"; 520val (stringN, string) = markup_elem "string"; 521val (alt_stringN, alt_string) = markup_elem "alt_string"; 522val (verbatimN, verbatim) = markup_elem "verbatim"; 523val (cartoucheN, cartouche) = markup_elem "cartouche"; 524val (commentN, comment) = markup_elem "comment"; 525 526 527(* timing *) 528 529val elapsedN = "elapsed"; 530val cpuN = "cpu"; 531val gcN = "gc"; 532 533fun timing_properties {elapsed, cpu, gc} = 534 [(elapsedN, Value.print_time elapsed), 535 (cpuN, Value.print_time cpu), 536 (gcN, Value.print_time gc)]; 537 538fun parse_timing_properties props = 539 {elapsed = Properties.seconds props elapsedN, 540 cpu = Properties.seconds props cpuN, 541 gc = Properties.seconds props gcN}; 542 543val timingN = "timing"; 544fun timing t = (timingN, timing_properties t); 545 546 547(* command timing *) 548 549val command_timingN = "command_timing"; 550 551fun command_timing_properties {file, offset, name} elapsed = 552 [(fileN, file), (offsetN, Value.print_int offset), 553 (nameN, name), (elapsedN, Value.print_time elapsed)]; 554 555fun parse_command_timing_properties props = 556 (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of 557 (SOME file, SOME offset, SOME name) => 558 SOME ({file = file, offset = Value.parse_int offset, name = name}, 559 Properties.seconds props elapsedN) 560 | _ => NONE); 561 562 563(* indentation *) 564 565val (command_indentN, command_indent) = markup_int "command_indent" indentN; 566 567 568(* goals *) 569 570val (goalN, goal) = markup_elem "goal"; 571val (subgoalN, subgoal) = markup_string "subgoal" nameN; 572 573 574(* command status *) 575 576val taskN = "task"; 577 578val (acceptedN, accepted) = markup_elem "accepted"; 579val (forkedN, forked) = markup_elem "forked"; 580val (joinedN, joined) = markup_elem "joined"; 581val (runningN, running) = markup_elem "running"; 582val (finishedN, finished) = markup_elem "finished"; 583val (failedN, failed) = markup_elem "failed"; 584 585val (initializedN, initialized) = markup_elem "initialized"; 586val (consolidatedN, consolidated) = markup_elem "consolidated"; 587 588 589(* messages *) 590 591val exec_idN = "exec_id"; 592 593val initN = "init"; 594val (statusN, status) = markup_elem "status"; 595val (resultN, result) = markup_elem "result"; 596val (writelnN, writeln) = markup_elem "writeln"; 597val (stateN, state) = markup_elem "state" 598val (informationN, information) = markup_elem "information"; 599val (tracingN, tracing) = markup_elem "tracing"; 600val (warningN, warning) = markup_elem "warning"; 601val (legacyN, legacy) = markup_elem "legacy"; 602val (errorN, error) = markup_elem "error"; 603val (systemN, system) = markup_elem "system"; 604val protocolN = "protocol"; 605 606val (reportN, report) = markup_elem "report"; 607val (no_reportN, no_report) = markup_elem "no_report"; 608 609val badN = "bad"; 610fun bad () = (badN, serial_properties (serial ())); 611 612val (intensifyN, intensify) = markup_elem "intensify"; 613 614 615(* active areas *) 616 617val browserN = "browser" 618val graphviewN = "graphview"; 619 620val sendbackN = "sendback"; 621val paddingN = "padding"; 622val padding_line = (paddingN, "line"); 623val padding_command = (paddingN, "command"); 624 625val dialogN = "dialog"; 626fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]); 627 628val jedit_actionN = "jedit_action"; 629 630 631(* protocol message functions *) 632 633val functionN = "function" 634 635val assign_update = [(functionN, "assign_update")]; 636val removed_versions = [(functionN, "removed_versions")]; 637 638fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)]; 639 640fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; 641fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; 642 643val ML_statistics = (functionN, "ML_statistics"); 644 645val task_statistics = (functionN, "task_statistics"); 646 647val command_timing = (functionN, "command_timing"); 648 649val theory_timing = (functionN, "theory_timing"); 650 651val exportN = "export"; 652type export_args = 653 {id: string option, serial: serial, theory_name: string, name: string, compress: bool} 654fun export ({id, serial, theory_name, name, compress}: export_args) = 655 [(functionN, exportN), (idN, the_default "" id), (serialN, Value.print_int serial), 656 ("theory_name", theory_name), (nameN, name), ("compress", Value.print_bool compress)]; 657 658fun loading_theory name = [("function", "loading_theory"), ("name", name)]; 659 660fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name 661 | dest_loading_theory _ = NONE; 662 663val build_session_finished = [("function", "build_session_finished")]; 664 665val print_operationsN = "print_operations"; 666val print_operations = [(functionN, print_operationsN)]; 667 668 669(* debugger *) 670 671fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)]; 672fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)]; 673 674 675(* simplifier trace *) 676 677val simp_trace_panelN = "simp_trace_panel"; 678 679val simp_trace_logN = "simp_trace_log"; 680val simp_trace_stepN = "simp_trace_step"; 681val simp_trace_recurseN = "simp_trace_recurse"; 682val simp_trace_hintN = "simp_trace_hint"; 683val simp_trace_ignoreN = "simp_trace_ignore"; 684 685fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)]; 686 687 688 689(** print mode operations **) 690 691val no_output = ("", ""); 692 693local 694 val default = {output = Output_Primitives.markup_fn}; 695 val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]); 696in 697 fun add_mode name output = 698 Synchronized.change modes (fn tab => 699 (if not (Symtab.defined tab name) then () 700 else Output.warning ("Redefining markup mode " ^ quote name); 701 Symtab.update (name, {output = output}) tab)); 702 fun get_mode () = 703 the_default default 704 (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); 705end; 706 707fun output m = if is_empty m then no_output else #output (get_mode ()) m; 708 709val enclose = output #-> Library.enclose; 710 711fun markup m = 712 let val (bg, en) = output m 713 in Library.enclose (Output.escape bg) (Output.escape en) end; 714 715val markups = fold_rev markup; 716 717fun markup_only m = markup m ""; 718 719fun markup_report "" = "" 720 | markup_report txt = markup report txt; 721 722end; 723