src/Pure/PIDE/isabelle_markup.ML
author wenzelm
Tue, 29 Nov 2011 21:50:00 +0100
changeset 45674 eb65c9d17e2f
parent 45670 b84170538043
child 46121 30a69cd8a9a0
permissions -rw-r--r--
clarified Time vs. Timing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45670
b84170538043 rearranged files;
wenzelm
parents: 45666
diff changeset
     1
(*  Title:      Pure/PIDE/isabelle_markup.ML
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     3
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
     4
Isabelle markup elements.
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     5
*)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     6
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
     7
signature ISABELLE_MARKUP =
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     8
sig
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
     9
  val bindingN: string val binding: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    10
  val entityN: string val entity: string -> string -> Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    11
  val get_entity_kind: Markup.T -> string option
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
    12
  val defN: string
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
    13
  val refN: string
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    14
  val lineN: string
27794
bdea6e17cbe3 added offset/end_offset;
wenzelm
parents: 27748
diff changeset
    15
  val offsetN: string
bdea6e17cbe3 added offset/end_offset;
wenzelm
parents: 27748
diff changeset
    16
  val end_offsetN: string
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    17
  val fileN: string
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
    18
  val idN: string
27748
c421ee0d2350 added position_properties';
wenzelm
parents: 27743
diff changeset
    19
  val position_properties': string list
26051
43bcb30a6d97 added position_properties;
wenzelm
parents: 26001
diff changeset
    20
  val position_properties: string list
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    21
  val positionN: string val position: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    22
  val pathN: string val path: string -> Markup.T
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
    23
  val indentN: string
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    24
  val blockN: string val block: int -> Markup.T
23695
6c4662bb4862 Add widthN to signature
aspinall
parents: 23671
diff changeset
    25
  val widthN: string
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    26
  val breakN: string val break: int -> Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    27
  val fbreakN: string val fbreak: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    28
  val hiddenN: string val hidden: Markup.T
43548
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43547
diff changeset
    29
  val classN: string
43552
156c822f181a entity markup for "type", "constant";
wenzelm
parents: 43548
diff changeset
    30
  val typeN: string
156c822f181a entity markup for "type", "constant";
wenzelm
parents: 43548
diff changeset
    31
  val constantN: string
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    32
  val fixedN: string val fixed: string -> Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    33
  val dynamic_factN: string val dynamic_fact: string -> Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    34
  val tfreeN: string val tfree: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    35
  val tvarN: string val tvar: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    36
  val freeN: string val free: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    37
  val skolemN: string val skolem: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    38
  val boundN: string val bound: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    39
  val varN: string val var: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    40
  val numeralN: string val numeral: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    41
  val literalN: string val literal: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    42
  val delimiterN: string val delimiter: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    43
  val inner_stringN: string val inner_string: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    44
  val inner_commentN: string val inner_comment: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    45
  val token_rangeN: string val token_range: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    46
  val sortN: string val sort: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    47
  val typN: string val typ: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    48
  val termN: string val term: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    49
  val propN: string val prop: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    50
  val typingN: string val typing: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    51
  val ML_keywordN: string val ML_keyword: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    52
  val ML_delimiterN: string val ML_delimiter: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    53
  val ML_tvarN: string val ML_tvar: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    54
  val ML_numeralN: string val ML_numeral: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    55
  val ML_charN: string val ML_char: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    56
  val ML_stringN: string val ML_string: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    57
  val ML_commentN: string val ML_comment: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    58
  val ML_malformedN: string val ML_malformed: Markup.T
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42135
diff changeset
    59
  val ML_defN: string
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42135
diff changeset
    60
  val ML_openN: string
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42135
diff changeset
    61
  val ML_structN: string
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    62
  val ML_typingN: string val ML_typing: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    63
  val ML_sourceN: string val ML_source: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    64
  val doc_sourceN: string val doc_source: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    65
  val antiqN: string val antiq: Markup.T
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43552
diff changeset
    66
  val ML_antiquotationN: string
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43560
diff changeset
    67
  val doc_antiquotationN: string
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43560
diff changeset
    68
  val doc_antiquotation_optionN: string
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    69
  val keyword_declN: string val keyword_decl: string -> Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    70
  val command_declN: string val command_decl: string -> string -> Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    71
  val keywordN: string val keyword: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    72
  val operatorN: string val operator: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    73
  val commandN: string val command: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    74
  val stringN: string val string: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    75
  val altstringN: string val altstring: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    76
  val verbatimN: string val verbatim: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    77
  val commentN: string val comment: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    78
  val controlN: string val control: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    79
  val malformedN: string val malformed: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    80
  val tokenN: string val token: Properties.T -> Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    81
  val command_spanN: string val command_span: string -> Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    82
  val ignored_spanN: string val ignored_span: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    83
  val malformed_spanN: string val malformed_span: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    84
  val loaded_theoryN: string val loaded_theory: string -> Markup.T
45674
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
    85
  val elapsedN: string
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
    86
  val cpuN: string
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
    87
  val gcN: string
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
    88
  val timingN: string val timing: Timing.timing -> Markup.T
38721
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
    89
  val subgoalsN: string
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    90
  val proof_stateN: string val proof_state: int -> Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    91
  val stateN: string val state: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    92
  val subgoalN: string val subgoal: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    93
  val sendbackN: string val sendback: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    94
  val hiliteN: string val hilite: Markup.T
29417
779ff1187327 added running task markup;
wenzelm
parents: 29325
diff changeset
    95
  val taskN: string
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    96
  val forkedN: string val forked: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    97
  val joinedN: string val joined: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    98
  val failedN: string val failed: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
    99
  val finishedN: string val finished: Markup.T
38871
28496da3bec2 message serial number indicates physical order;
wenzelm
parents: 38721
diff changeset
   100
  val serialN: string
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   101
  val legacyN: string val legacy: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   102
  val promptN: string val prompt: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   103
  val readyN: string val ready: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   104
  val reportN: string val report: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   105
  val no_reportN: string val no_report: Markup.T
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   106
  val badN: string val bad: Markup.T
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43710
diff changeset
   107
  val functionN: string
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44549
diff changeset
   108
  val assign_execs: Properties.T
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   109
  val removed_versions: Properties.T
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43710
diff changeset
   110
  val invoke_scala: string -> string -> Properties.T
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 43797
diff changeset
   111
  val cancel_scala: string -> Properties.T
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   112
end;
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   113
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   114
structure Isabelle_Markup: ISABELLE_MARKUP =
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   115
struct
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   116
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
   117
(** markup elements **)
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
   118
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   119
fun markup_elem elem = (elem, (elem, []): Markup.T);
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   120
fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): Markup.T);
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   121
fun markup_int elem prop = (elem, fn i => (elem, [(prop, Markup.print_int i)]): Markup.T);
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   122
23658
wenzelm
parents: 23644
diff changeset
   123
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   124
(* formal entities *)
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   125
43547
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 43432
diff changeset
   126
val (bindingN, binding) = markup_elem "binding";
42135
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 42012
diff changeset
   127
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 42012
diff changeset
   128
val entityN = "entity";
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   129
fun entity kind name = (entityN, [(Markup.nameN, name), (Markup.kindN, kind)]);
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   130
43548
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43547
diff changeset
   131
fun get_entity_kind (name, props) =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   132
  if name = entityN then AList.lookup (op =) props Markup.kindN
43548
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43547
diff changeset
   133
  else NONE;
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43547
diff changeset
   134
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   135
val defN = "def";
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   136
val refN = "ref";
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   137
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   138
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   139
(* position *)
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   140
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   141
val lineN = "line";
27794
bdea6e17cbe3 added offset/end_offset;
wenzelm
parents: 27748
diff changeset
   142
val offsetN = "offset";
bdea6e17cbe3 added offset/end_offset;
wenzelm
parents: 27748
diff changeset
   143
val end_offsetN = "end_offset";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   144
val fileN = "file";
25816
d2a94e6a7d1e moved id to position properties;
wenzelm
parents: 25808
diff changeset
   145
val idN = "id";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   146
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
   147
val position_properties' = [fileN, idN];
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 43684
diff changeset
   148
val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
27748
c421ee0d2350 added position_properties';
wenzelm
parents: 27743
diff changeset
   149
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   150
val (positionN, position) = markup_elem "position";
26255
2246d8bbe89d added location;
wenzelm
parents: 26051
diff changeset
   151
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   152
43593
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   153
(* path *)
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   154
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   155
val (pathN, path) = markup_string "path" Markup.nameN;
43593
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   156
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   157
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   158
(* pretty printing *)
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   159
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   160
val indentN = "indent";
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   161
val (blockN, block) = markup_int "block" indentN;
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   162
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   163
val widthN = "width";
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   164
val (breakN, break) = markup_int "break" widthN;
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   165
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   166
val (fbreakN, fbreak) = markup_elem "fbreak";
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   167
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   168
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33643
diff changeset
   169
(* hidden text *)
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33643
diff changeset
   170
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33643
diff changeset
   171
val (hiddenN, hidden) = markup_elem "hidden";
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33643
diff changeset
   172
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33643
diff changeset
   173
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   174
(* logical entities *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   175
43548
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43547
diff changeset
   176
val classN = "class";
43552
156c822f181a entity markup for "type", "constant";
wenzelm
parents: 43548
diff changeset
   177
val typeN = "type";
156c822f181a entity markup for "type", "constant";
wenzelm
parents: 43548
diff changeset
   178
val constantN = "constant";
156c822f181a entity markup for "type", "constant";
wenzelm
parents: 43548
diff changeset
   179
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   180
val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   181
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" Markup.nameN;
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   182
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   183
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   184
(* inner syntax *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   185
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   186
val (tfreeN, tfree) = markup_elem "tfree";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   187
val (tvarN, tvar) = markup_elem "tvar";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   188
val (freeN, free) = markup_elem "free";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   189
val (skolemN, skolem) = markup_elem "skolem";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   190
val (boundN, bound) = markup_elem "bound";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   191
val (varN, var) = markup_elem "var";
29318
6337d1cb2ba0 added numeral, which supercedes num, xnum, float;
wenzelm
parents: 28904
diff changeset
   192
val (numeralN, numeral) = markup_elem "numeral";
27804
f682666352c4 added literal;
wenzelm
parents: 27794
diff changeset
   193
val (literalN, literal) = markup_elem "literal";
43432
224006e5ac46 inner literal/delimiter corresponds to outer keyword/operator;
wenzelm
parents: 42492
diff changeset
   194
val (delimiterN, delimiter) = markup_elem "delimiter";
29318
6337d1cb2ba0 added numeral, which supercedes num, xnum, float;
wenzelm
parents: 28904
diff changeset
   195
val (inner_stringN, inner_string) = markup_elem "inner_string";
27883
e506f0c6d3f0 added is_none;
wenzelm
parents: 27879
diff changeset
   196
val (inner_commentN, inner_comment) = markup_elem "inner_comment";
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   197
39168
e3ac771235f7 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents: 38887
diff changeset
   198
val (token_rangeN, token_range) = markup_elem "token_range";
e3ac771235f7 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents: 38887
diff changeset
   199
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   200
val (sortN, sort) = markup_elem "sort";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   201
val (typN, typ) = markup_elem "typ";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   202
val (termN, term) = markup_elem "term";
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
   203
val (propN, prop) = markup_elem "prop";
27748
c421ee0d2350 added position_properties';
wenzelm
parents: 27743
diff changeset
   204
45445
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44706
diff changeset
   205
val (typingN, typing) = markup_elem "typing";
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44706
diff changeset
   206
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   207
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   208
(* ML syntax *)
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   209
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   210
val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
37195
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 37193
diff changeset
   211
val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   212
val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   213
val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   214
val (ML_charN, ML_char) = markup_elem "ML_char";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   215
val (ML_stringN, ML_string) = markup_elem "ML_string";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   216
val (ML_commentN, ML_comment) = markup_elem "ML_comment";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   217
val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   218
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42135
diff changeset
   219
val ML_defN = "ML_def";
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42135
diff changeset
   220
val ML_openN = "ML_open";
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42135
diff changeset
   221
val ML_structN = "ML_struct";
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30614
diff changeset
   222
val (ML_typingN, ML_typing) = markup_elem "ML_typing";
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30614
diff changeset
   223
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   224
27875
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   225
(* embedded source text *)
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   226
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   227
val (ML_sourceN, ML_source) = markup_elem "ML_source";
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   228
val (doc_sourceN, doc_source) = markup_elem "doc_source";
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   229
27879
wenzelm
parents: 27875
diff changeset
   230
val (antiqN, antiq) = markup_elem "antiq";
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43552
diff changeset
   231
val ML_antiquotationN = "ML antiquotation";
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43560
diff changeset
   232
val doc_antiquotationN = "document antiquotation";
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43560
diff changeset
   233
val doc_antiquotation_optionN = "document antiquotation option";
27879
wenzelm
parents: 27875
diff changeset
   234
27875
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   235
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   236
(* outer syntax *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   237
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   238
val (keyword_declN, keyword_decl) = markup_string "keyword_decl" Markup.nameN;
24870
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   239
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   240
val command_declN = "command_decl";
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   241
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   242
fun command_decl name kind : Markup.T =
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   243
  (command_declN, [(Markup.nameN, name), (Markup.kindN, kind)]);
24870
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   244
37193
a4b2bb0dab08 simplified command/keyword markup;
wenzelm
parents: 37192
diff changeset
   245
val (keywordN, keyword) = markup_elem "keyword";
37192
8cdddd689ea9 markup non-identifier keyword as operator;
wenzelm
parents: 37186
diff changeset
   246
val (operatorN, operator) = markup_elem "operator";
37193
a4b2bb0dab08 simplified command/keyword markup;
wenzelm
parents: 37192
diff changeset
   247
val (commandN, command) = markup_elem "command";
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   248
val (stringN, string) = markup_elem "string";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   249
val (altstringN, altstring) = markup_elem "altstring";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   250
val (verbatimN, verbatim) = markup_elem "verbatim";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   251
val (commentN, comment) = markup_elem "comment";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   252
val (controlN, control) = markup_elem "control";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   253
val (malformedN, malformed) = markup_elem "malformed";
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   254
38229
61d0fe8b96ac more robust treatment of Markup.token;
wenzelm
parents: 37195
diff changeset
   255
val tokenN = "token";
61d0fe8b96ac more robust treatment of Markup.token;
wenzelm
parents: 37195
diff changeset
   256
fun token props = (tokenN, props);
27851
wenzelm
parents: 27836
diff changeset
   257
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   258
val (command_spanN, command_span) = markup_string "command_span" Markup.nameN;
27660
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
   259
val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
27836
74e8228757c5 renamed unknown_span to malformed_span;
wenzelm
parents: 27828
diff changeset
   260
val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   261
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   262
43673
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43665
diff changeset
   263
(* theory loader *)
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43665
diff changeset
   264
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   265
val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" Markup.nameN;
40394
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40391
diff changeset
   266
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40391
diff changeset
   267
45674
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   268
(* timing *)
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   269
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   270
val timingN = "timing";
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   271
val elapsedN = "elapsed";
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   272
val cpuN = "cpu";
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   273
val gcN = "gc";
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   274
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   275
fun timing {elapsed, cpu, gc} =
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   276
  (timingN,
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   277
   [(elapsedN, Time.toString elapsed),
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   278
    (cpuN, Time.toString cpu),
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   279
    (gcN, Time.toString gc)]);
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   280
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   281
40394
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40391
diff changeset
   282
(* toplevel *)
40391
b0dafbfc05b7 explicit "timing" status for toplevel transactions;
wenzelm
parents: 40131
diff changeset
   283
38721
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   284
val subgoalsN = "subgoals";
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   285
val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   286
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   287
val (stateN, state) = markup_elem "state";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   288
val (subgoalN, subgoal) = markup_elem "subgoal";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   289
val (sendbackN, sendback) = markup_elem "sendback";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   290
val (hiliteN, hilite) = markup_elem "hilite";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   291
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   292
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   293
(* command status *)
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   294
29417
779ff1187327 added running task markup;
wenzelm
parents: 29325
diff changeset
   295
val taskN = "task";
779ff1187327 added running task markup;
wenzelm
parents: 29325
diff changeset
   296
37186
349e9223c685 explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents: 34242
diff changeset
   297
val (forkedN, forked) = markup_elem "forked";
349e9223c685 explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents: 34242
diff changeset
   298
val (joinedN, joined) = markup_elem "joined";
38429
9951852fae91 simplified command status: interpret stacked markup on demand;
wenzelm
parents: 38414
diff changeset
   299
27615
wenzelm
parents: 27606
diff changeset
   300
val (failedN, failed) = markup_elem "failed";
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   301
val (finishedN, finished) = markup_elem "finished";
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   302
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   303
27969
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   304
(* messages *)
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   305
38871
28496da3bec2 message serial number indicates physical order;
wenzelm
parents: 38721
diff changeset
   306
val serialN = "serial";
27969
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   307
44549
5e5e6ad3922c explicit markup for legacy warnings;
wenzelm
parents: 44476
diff changeset
   308
val (legacyN, legacy) = markup_elem "legacy";
27969
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   309
val (promptN, prompt) = markup_elem "prompt";
31384
ce169bd37fc0 IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents: 30702
diff changeset
   310
val (readyN, ready) = markup_elem "ready";
27969
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   311
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
   312
val (reportN, report) = markup_elem "report";
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39171
diff changeset
   313
val (no_reportN, no_report) = markup_elem "no_report";
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38871
diff changeset
   314
39171
525a13b9ac74 highlight bad range of nested error (here from inner parsing);
wenzelm
parents: 39168
diff changeset
   315
val (badN, bad) = markup_elem "bad";
525a13b9ac74 highlight bad range of nested error (here from inner parsing);
wenzelm
parents: 39168
diff changeset
   316
27969
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   317
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43710
diff changeset
   318
(* raw message functions *)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43710
diff changeset
   319
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43710
diff changeset
   320
val functionN = "function"
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43710
diff changeset
   321
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44549
diff changeset
   322
val assign_execs = [(functionN, "assign_execs")];
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   323
val removed_versions = [(functionN, "removed_versions")];
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44549
diff changeset
   324
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
   325
fun invoke_scala name id = [(functionN, "invoke_scala"), (Markup.nameN, name), (idN, id)];
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 43797
diff changeset
   326
fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43710
diff changeset
   327
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   328
end;