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