src/Pure/PIDE/markup.ML
author wenzelm
Mon, 05 May 2014 15:17:07 +0200
changeset 56864 0446c7ac2e32
parent 56743 81370dfadb1d
child 57594 037f3b251df5
permissions -rw-r--r--
support print operations as asynchronous query;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45670
b84170538043 rearranged files;
wenzelm
parents: 45666
diff changeset
     1
(*  Title:      Pure/PIDE/markup.ML
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     3
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
     4
Quasi-abstract markup elements.
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     5
*)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     6
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     7
signature MARKUP =
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     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
a9725750c53a more uniform Markup.parse_real;
wenzelm
parents: 51951
diff changeset
    13
  val parse_real: string -> real
a9725750c53a more uniform Markup.parse_real;
wenzelm
parents: 51951
diff changeset
    14
  val print_real: real -> string
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27969
diff changeset
    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
61d0fe8b96ac more robust treatment of Markup.token;
wenzelm
parents: 37195
diff changeset
    18
  val properties: Properties.T -> T -> T
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    19
  val nameN: string
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
    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
513c2b0ea565 more markup;
wenzelm
parents: 55956
diff changeset
    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
ad446b45efff more markup;
wenzelm
parents: 55561
diff changeset
    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
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    50
  val offsetN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    51
  val end_offsetN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    52
  val fileN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    53
  val idN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    54
  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
    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 positionN: string val position: T
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    57
  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
    58
  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
    59
  val indentN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    60
  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
    61
  val widthN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    62
  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
    63
  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
    64
  val itemN: string val item: T
56548
ae6870efc28d markup for prose words within formal comments;
wenzelm
parents: 56465
diff changeset
    65
  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
    66
  val hiddenN: string val hidden: T
56465
6ad693903e22 more positions and markup;
wenzelm
parents: 56278
diff changeset
    67
  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
    68
  val theoryN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    69
  val classN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    70
  val type_nameN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    71
  val constantN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    72
  val fixedN: string val fixed: string -> T
53378
07990ba8c0ea cases: more position information and PIDE markup;
wenzelm
parents: 53055
diff changeset
    73
  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
    74
  val dynamic_factN: string val dynamic_fact: string -> T
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    75
  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
    76
  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
    77
  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
    78
  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
    79
  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
    80
  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
    81
  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
    82
  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
    83
  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
    84
  val inner_stringN: string val inner_string: T
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54702
diff changeset
    85
  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
    86
  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
    87
  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
    88
  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
    89
  val typingN: string val typing: T
55505
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55033
diff changeset
    90
  val ML_keyword1N: string val ML_keyword1: T
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55033
diff changeset
    91
  val ML_keyword2N: string val ML_keyword2: T
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55033
diff changeset
    92
  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
    93
  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
    94
  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
    95
  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
    96
  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
    97
  val ML_stringN: string val ML_string: T
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
    98
  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
    99
  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
   100
  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
   101
  val ML_defN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   102
  val ML_openN: string
55837
154855d9a564 clarified names of antiquotations and markup;
wenzelm
parents: 55828
diff changeset
   103
  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
   104
  val ML_typingN: string val ML_typing: T
55526
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   105
  val antiquotedN: string val antiquoted: T
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   106
  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
   107
  val ML_antiquotationN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   108
  val document_antiquotationN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   109
  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
   110
  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
   111
  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
   112
  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
   113
  val stringN: string val string: T
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   114
  val altstringN: string val altstring: T
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   115
  val verbatimN: string val verbatim: T
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54702
diff changeset
   116
  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
   117
  val commentN: string val comment: T
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   118
  val controlN: string val control: T
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   119
  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
   120
  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
   121
  val keyword2N: string val keyword2: T
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 55761
diff changeset
   122
  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
   123
  val quasi_keywordN: string val quasi_keyword: T
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56034
diff changeset
   124
  val improperN: string val improper: T
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56034
diff changeset
   125
  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
   126
  val elapsedN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   127
  val cpuN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   128
  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
   129
  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
   130
  val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time}
51228
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   131
  val command_timingN: string
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   132
  val command_timing_properties:
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   133
    {file: string, offset: int, name: string} -> Time.time -> Properties.T
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   134
  val parse_command_timing_properties:
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   135
    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
   136
  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
   137
  val subgoalsN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   138
  val proof_stateN: string val proof_state: int -> T
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   139
  val stateN: string val state: T
50543
42bbe637be54 fold main goal;
wenzelm
parents: 50537
diff changeset
   140
  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
   141
  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
   142
  val taskN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   143
  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
   144
  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
   145
  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
   146
  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
   147
  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
   148
  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
   149
  val serialN: string
52854
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
   150
  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
   151
  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
   152
  val initN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   153
  val statusN: string
50503
50f141b34bb7 enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents: 50500
diff changeset
   154
  val resultN: string
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   155
  val writelnN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   156
  val tracingN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   157
  val warningN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   158
  val errorN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   159
  val protocolN: string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   160
  val legacyN: string val legacy: T
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   161
  val promptN: string val prompt: T
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   162
  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
   163
  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
   164
  val badN: string val bad: T
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   165
  val intensifyN: string val intensify: T
52643
34c29356930e more explicit Markup.information for messages produced by "auto" tools;
wenzelm
parents: 52563
diff changeset
   166
  val informationN: string val information: T
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50683
diff changeset
   167
  val browserN: string
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   168
  val graphviewN: string
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   169
  val sendbackN: string
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   170
  val paddingN: string
50842
777c6026ca93 tuned signature;
wenzelm
parents: 50781
diff changeset
   171
  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
   172
  val padding_command: Properties.entry
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   173
  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
   174
  val functionN: string
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52111
diff changeset
   175
  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
   176
  val removed_versions: Properties.T
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51990
diff changeset
   177
  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
   178
  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
   179
  val cancel_scala: string -> Properties.T
50842
777c6026ca93 tuned signature;
wenzelm
parents: 50781
diff changeset
   180
  val ML_statistics: Properties.entry
50975
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50914
diff changeset
   181
  val task_statistics: Properties.entry
51216
e6e7685fc8f8 emit command_timing properties into build log;
wenzelm
parents: 50975
diff changeset
   182
  val command_timing: Properties.entry
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50842
diff changeset
   183
  val loading_theory: string -> Properties.T
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50842
diff changeset
   184
  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
   185
  val use_theories_result: string -> bool -> Properties.T
56864
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56743
diff changeset
   186
  val print_operationsN: string
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56743
diff changeset
   187
  val print_operations: Properties.T
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   188
  val simp_trace_logN: string
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   189
  val simp_trace_stepN: string
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   190
  val simp_trace_recurseN: string
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   191
  val simp_trace_hintN: string
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   192
  val simp_trace_ignoreN: string
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   193
  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
   194
  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
   195
  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
   196
  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
   197
  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
   198
  val enclose: T -> Output.output -> Output.output
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   199
  val markup: T -> string -> string
43665
573d1272f36d tuned signature;
wenzelm
parents: 43593
diff changeset
   200
  val markup_only: T -> string
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55919
diff changeset
   201
  val markup_report: string -> string
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   202
end;
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   203
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   204
structure Markup: MARKUP =
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   205
struct
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   206
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
   207
(** markup elements **)
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
   208
51988
a9725750c53a more uniform Markup.parse_real;
wenzelm
parents: 51951
diff changeset
   209
(* misc values *)
51951
fab4ab92e812 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents: 51665
diff changeset
   210
fab4ab92e812 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents: 51665
diff changeset
   211
fun parse_bool "true" = true
fab4ab92e812 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents: 51665
diff changeset
   212
  | parse_bool "false" = false
fab4ab92e812 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents: 51665
diff changeset
   213
  | parse_bool s = raise Fail ("Bad boolean: " ^ quote s);
fab4ab92e812 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents: 51665
diff changeset
   214
fab4ab92e812 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents: 51665
diff changeset
   215
val print_bool = Bool.toString;
fab4ab92e812 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents: 51665
diff changeset
   216
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
   217
fun parse_int s =
43797
fad7758421bf more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents: 43748
diff changeset
   218
  let val i = Int.fromString s in
fad7758421bf more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents: 43748
diff changeset
   219
    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
   220
    then raise Fail ("Bad integer: " ^ quote s)
fad7758421bf more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents: 43748
diff changeset
   221
    else the i
fad7758421bf more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents: 43748
diff changeset
   222
  end;
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
   223
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
   224
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
   225
51988
a9725750c53a more uniform Markup.parse_real;
wenzelm
parents: 51951
diff changeset
   226
fun parse_real s =
a9725750c53a more uniform Markup.parse_real;
wenzelm
parents: 51951
diff changeset
   227
  (case Real.fromString s of
a9725750c53a more uniform Markup.parse_real;
wenzelm
parents: 51951
diff changeset
   228
    SOME x => x
a9725750c53a more uniform Markup.parse_real;
wenzelm
parents: 51951
diff changeset
   229
  | NONE => raise Fail ("Bad real: " ^ quote s));
a9725750c53a more uniform Markup.parse_real;
wenzelm
parents: 51951
diff changeset
   230
51990
cc66addbba6d more uniform Markup.print_real;
wenzelm
parents: 51988
diff changeset
   231
fun print_real x =
cc66addbba6d more uniform Markup.print_real;
wenzelm
parents: 51988
diff changeset
   232
  let val s = signed_string_of_real x in
cc66addbba6d more uniform Markup.print_real;
wenzelm
parents: 51988
diff changeset
   233
    (case space_explode "." s of
cc66addbba6d more uniform Markup.print_real;
wenzelm
parents: 51988
diff changeset
   234
      [a, b] => if forall_string (fn c => c = "0") b then a else s
cc66addbba6d more uniform Markup.print_real;
wenzelm
parents: 51988
diff changeset
   235
    | _ => s)
cc66addbba6d more uniform Markup.print_real;
wenzelm
parents: 51988
diff changeset
   236
  end;
51988
a9725750c53a more uniform Markup.parse_real;
wenzelm
parents: 51951
diff changeset
   237
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
   238
23658
wenzelm
parents: 23644
diff changeset
   239
(* basic markup *)
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   240
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27969
diff changeset
   241
type T = string * Properties.T;
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   242
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
   243
val empty = ("", []);
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   244
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
   245
fun is_empty ("", _) = true
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
   246
  | is_empty _ = false;
27883
e506f0c6d3f0 added is_none;
wenzelm
parents: 27879
diff changeset
   247
23794
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
   248
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   249
fun properties more_props ((elem, props): T) =
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27969
diff changeset
   250
  (elem, fold_rev Properties.put more_props props);
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   251
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   252
fun markup_elem name = (name, (name, []): T);
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   253
fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T);
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   254
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
   255
26977
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
   256
38721
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   257
(* misc properties *)
26977
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
   258
23658
wenzelm
parents: 23644
diff changeset
   259
val nameN = "name";
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
   260
fun name a = properties [(nameN, a)];
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
   261
23658
wenzelm
parents: 23644
diff changeset
   262
val kindN = "kind";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   263
52854
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
   264
val instanceN = "instance";
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
   265
23658
wenzelm
parents: 23644
diff changeset
   266
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   267
(* embedded languages *)
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   268
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   269
val languageN = "language";
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55613
diff changeset
   270
val symbolsN = "symbols";
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55653
diff changeset
   271
val antiquotesN = "antiquotes";
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   272
val delimitedN = "delimited"
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   273
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   274
fun is_delimited props =
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   275
  Properties.get props delimitedN = SOME "true";
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55653
diff changeset
   276
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   277
fun language {name, symbols, antiquotes, delimited} =
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55653
diff changeset
   278
  (languageN,
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   279
   [(nameN, name),
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   280
    (symbolsN, print_bool symbols),
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   281
    (antiquotesN, print_bool antiquotes),
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   282
    (delimitedN, print_bool delimited)]);
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   283
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   284
fun language' {name, symbols, antiquotes} delimited =
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   285
  language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   286
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   287
val language_method =
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   288
  language {name = "method", symbols = true, antiquotes = false, delimited = false};
56033
513c2b0ea565 more markup;
wenzelm
parents: 55956
diff changeset
   289
val language_attribute =
513c2b0ea565 more markup;
wenzelm
parents: 55956
diff changeset
   290
  language {name = "attribute", symbols = true, antiquotes = false, delimited = false};
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   291
val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   292
val language_type = language' {name = "type", symbols = true, antiquotes = false};
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   293
val language_term = language' {name = "term", symbols = true, antiquotes = false};
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   294
val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   295
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
   296
val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   297
val language_document = language' {name = "document", symbols = false, antiquotes = true};
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   298
val language_antiquotation =
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   299
  language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   300
val language_text = language' {name = "text", symbols = true, antiquotes = false};
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   301
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
   302
val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true};
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   303
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   304
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   305
(* formal entities *)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   306
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   307
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
   308
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   309
val entityN = "entity";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   310
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
   311
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   312
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
   313
  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
   314
  else NONE;
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   315
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   316
val defN = "def";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   317
val refN = "ref";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   318
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   319
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
   320
(* completion *)
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
   321
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
   322
val (completionN, completion) = markup_elem "completion";
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55837
diff changeset
   323
val (no_completionN, no_completion) = markup_elem "no_completion";
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
   324
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
   325
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   326
(* position *)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   327
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   328
val lineN = "line";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   329
val offsetN = "offset";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   330
val end_offsetN = "end_offset";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   331
val fileN = "file";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   332
val idN = "id";
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 position_properties' = [fileN, idN];
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   335
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
   336
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   337
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
   338
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   339
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53378
diff changeset
   340
(* external resources *)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   341
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   342
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
   343
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
   344
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
(* pretty printing *)
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
val indentN = "indent";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   349
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
   350
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   351
val widthN = "width";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   352
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
   353
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   354
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
   355
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
   356
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
   357
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   358
56548
ae6870efc28d markup for prose words within formal comments;
wenzelm
parents: 56465
diff changeset
   359
(* text properties *)
ae6870efc28d markup for prose words within formal comments;
wenzelm
parents: 56465
diff changeset
   360
ae6870efc28d markup for prose words within formal comments;
wenzelm
parents: 56465
diff changeset
   361
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
   362
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   363
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
   364
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   365
56465
6ad693903e22 more positions and markup;
wenzelm
parents: 56278
diff changeset
   366
(* formal entities *)
6ad693903e22 more positions and markup;
wenzelm
parents: 56278
diff changeset
   367
6ad693903e22 more positions and markup;
wenzelm
parents: 56278
diff changeset
   368
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
   369
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   370
val theoryN = "theory";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   371
val classN = "class";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   372
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
   373
val constantN = "constant";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   374
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   375
val (fixedN, fixed) = markup_string "fixed" nameN;
53378
07990ba8c0ea cases: more position information and PIDE markup;
wenzelm
parents: 53055
diff changeset
   376
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
   377
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
   378
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   379
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   380
(* inner syntax *)
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 (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
   383
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
   384
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
   385
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
   386
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
   387
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
   388
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
   389
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
   390
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
   391
val (inner_stringN, inner_string) = markup_elem "inner_string";
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54702
diff changeset
   392
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
   393
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
   394
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   395
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
   396
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   397
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
   398
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
   399
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
(* ML syntax *)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   402
55505
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55033
diff changeset
   403
val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55033
diff changeset
   404
val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2";
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55033
diff changeset
   405
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
   406
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
   407
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
   408
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
   409
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
   410
val (ML_stringN, ML_string) = markup_elem "ML_string";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   411
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
   412
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
   413
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
   414
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   415
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
   416
val ML_openN = "ML_open";
55837
154855d9a564 clarified names of antiquotations and markup;
wenzelm
parents: 55828
diff changeset
   417
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
   418
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
   419
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   420
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   421
(* antiquotations *)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   422
55526
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   423
val (antiquotedN, antiquoted) = markup_elem "antiquoted";
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   424
val (antiquoteN, antiquote) = markup_elem "antiquote";
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   425
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   426
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
   427
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
   428
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
   429
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   430
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   431
(* text structure *)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   432
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   433
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
   434
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
   435
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
(* outer syntax *)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   438
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
   439
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
   440
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
   441
val (keyword2N, keyword2) = markup_elem "keyword2";
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 55761
diff changeset
   442
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
   443
val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword";
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56034
diff changeset
   444
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
   445
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
   446
val (stringN, string) = markup_elem "string";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   447
val (altstringN, altstring) = markup_elem "altstring";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   448
val (verbatimN, verbatim) = markup_elem "verbatim";
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54702
diff changeset
   449
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
   450
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
   451
val (controlN, control) = markup_elem "control";
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
val tokenN = "token";
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55763
diff changeset
   454
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
   455
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   456
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   457
(* timing *)
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
val elapsedN = "elapsed";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   460
val cpuN = "cpu";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   461
val gcN = "gc";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   462
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   463
fun timing_properties {elapsed, cpu, gc} =
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   464
 [(elapsedN, Time.toString elapsed),
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   465
  (cpuN, Time.toString cpu),
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   466
  (gcN, Time.toString gc)];
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   467
51665
cba83c9f72b9 tuned signature;
wenzelm
parents: 51626
diff changeset
   468
fun parse_timing_properties props =
cba83c9f72b9 tuned signature;
wenzelm
parents: 51626
diff changeset
   469
 {elapsed = Properties.seconds props elapsedN,
cba83c9f72b9 tuned signature;
wenzelm
parents: 51626
diff changeset
   470
  cpu = Properties.seconds props cpuN,
cba83c9f72b9 tuned signature;
wenzelm
parents: 51626
diff changeset
   471
  gc = Properties.seconds props gcN};
51218
6425a0d3b7ac support for build passing timings from Scala to ML;
wenzelm
parents: 51217
diff changeset
   472
51665
cba83c9f72b9 tuned signature;
wenzelm
parents: 51626
diff changeset
   473
val timingN = "timing";
cba83c9f72b9 tuned signature;
wenzelm
parents: 51626
diff changeset
   474
fun timing t = (timingN, timing_properties t);
51218
6425a0d3b7ac support for build passing timings from Scala to ML;
wenzelm
parents: 51217
diff changeset
   475
51228
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   476
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   477
(* command timing *)
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   478
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   479
val command_timingN = "command_timing";
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   480
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   481
fun command_timing_properties {file, offset, name} elapsed =
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   482
 [(fileN, file), (offsetN, print_int offset),
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   483
  (nameN, name), (elapsedN, Time.toString elapsed)];
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   484
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   485
fun parse_command_timing_properties props =
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   486
  (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   487
    (SOME file, SOME offset, SOME name) =>
51665
cba83c9f72b9 tuned signature;
wenzelm
parents: 51626
diff changeset
   488
      SOME ({file = file, offset = parse_int offset, name = name},
cba83c9f72b9 tuned signature;
wenzelm
parents: 51626
diff changeset
   489
        Properties.seconds props elapsedN)
51228
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   490
  | _ => NONE);
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   491
dff3471dd8bc more tight representation of command timing;
wenzelm
parents: 51218
diff changeset
   492
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   493
(* toplevel *)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   494
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   495
val subgoalsN = "subgoals";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   496
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
   497
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   498
val (stateN, state) = markup_elem "state";
50543
42bbe637be54 fold main goal;
wenzelm
parents: 50537
diff changeset
   499
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
   500
val (subgoalN, subgoal) = markup_string "subgoal" nameN;
50215
97959912840a more general sendback properties;
wenzelm
parents: 50201
diff changeset
   501
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50255
diff changeset
   502
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   503
(* command status *)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   504
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   505
val taskN = "task";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   506
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   507
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
   508
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
   509
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
   510
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
   511
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
   512
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
   513
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   514
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   515
(* messages *)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   516
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   517
val serialN = "serial";
52854
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
   518
fun serial_properties i = [(serialN, print_int i)];
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
   519
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50845
diff changeset
   520
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
   521
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   522
val initN = "init";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   523
val statusN = "status";
50503
50f141b34bb7 enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents: 50500
diff changeset
   524
val resultN = "result";
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   525
val writelnN = "writeln";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   526
val tracingN = "tracing";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   527
val warningN = "warning";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   528
val errorN = "error";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   529
val protocolN = "protocol";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   530
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   531
val (legacyN, legacy) = markup_elem "legacy";
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   532
val (promptN, prompt) = markup_elem "prompt";
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
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
   535
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
   536
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   537
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
   538
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   539
val (intensifyN, intensify) = markup_elem "intensify";
52643
34c29356930e more explicit Markup.information for messages produced by "auto" tools;
wenzelm
parents: 52563
diff changeset
   540
val (informationN, information) = markup_elem "information";
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   541
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   542
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   543
(* active areas *)
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   544
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50683
diff changeset
   545
val browserN = "browser"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   546
val graphviewN = "graphview";
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   547
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   548
val sendbackN = "sendback";
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   549
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
   550
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
   551
val padding_command = (paddingN, "command");
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   552
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   553
val dialogN = "dialog";
50503
50f141b34bb7 enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents: 50500
diff changeset
   554
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
   555
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   556
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   557
(* protocol message functions *)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   558
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   559
val functionN = "function"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   560
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52111
diff changeset
   561
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
   562
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
   563
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51990
diff changeset
   564
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
   565
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 46894
diff changeset
   566
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
   567
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
   568
50683
34b109c5324c inline ML statistics into build log;
wenzelm
parents: 50545
diff changeset
   569
val ML_statistics = (functionN, "ML_statistics");
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   570
50975
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50914
diff changeset
   571
val task_statistics = (functionN, "task_statistics");
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50914
diff changeset
   572
51216
e6e7685fc8f8 emit command_timing properties into build log;
wenzelm
parents: 50975
diff changeset
   573
val command_timing = (functionN, "command_timing");
e6e7685fc8f8 emit command_timing properties into build log;
wenzelm
parents: 50975
diff changeset
   574
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50842
diff changeset
   575
fun loading_theory name = [("function", "loading_theory"), ("name", name)];
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50842
diff changeset
   576
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50842
diff changeset
   577
fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50842
diff changeset
   578
  | dest_loading_theory _ = NONE;
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50842
diff changeset
   579
56616
abc2da18d08d added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents: 56548
diff changeset
   580
fun use_theories_result id ok =
abc2da18d08d added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents: 56548
diff changeset
   581
  [("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
   582
56864
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56743
diff changeset
   583
val print_operationsN = "print_operations";
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56743
diff changeset
   584
val print_operations = [(functionN, print_operationsN)];
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56743
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
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   587
(* simplifier trace *)
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   588
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   589
val simp_trace_logN = "simp_trace_log";
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   590
val simp_trace_stepN = "simp_trace_step";
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   591
val simp_trace_recurseN = "simp_trace_recurse";
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   592
val simp_trace_hintN = "simp_trace_hint";
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   593
val simp_trace_ignoreN = "simp_trace_ignore";
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   594
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   595
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
   596
27969
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   597
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
   598
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
   599
(** print mode operations **)
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   600
29325
a205acc94356 Markup.no_output;
wenzelm
parents: 29318
diff changeset
   601
val no_output = ("", "");
a205acc94356 Markup.no_output;
wenzelm
parents: 29318
diff changeset
   602
fun default_output (_: T) = no_output;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   603
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   604
local
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   605
  val default = {output = default_output};
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
   606
  val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   607
in
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
   608
  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
   609
    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
   610
      (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
   611
       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
   612
       Symtab.update (name, {output = output}) tab));
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   613
  fun get_mode () =
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
   614
    the_default default
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
   615
      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   616
end;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   617
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
   618
fun output m = if is_empty m then no_output else #output (get_mode ()) m;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   619
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   620
val enclose = output #-> Library.enclose;
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   621
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   622
fun markup m =
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   623
  let val (bg, en) = output m
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   624
  in Library.enclose (Output.escape bg) (Output.escape en) end;
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   625
43665
573d1272f36d tuned signature;
wenzelm
parents: 43593
diff changeset
   626
fun markup_only m = markup m "";
573d1272f36d tuned signature;
wenzelm
parents: 43593
diff changeset
   627
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55919
diff changeset
   628
fun markup_report "" = ""
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55919
diff changeset
   629
  | markup_report txt = markup report txt;
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55919
diff changeset
   630
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   631
end;