src/Pure/General/markup.ML
author wenzelm
Tue, 05 Aug 2008 13:31:36 +0200
changeset 27740 0b22524c05e2
parent 27735 044901e02cc6
child 27743 7420e78f1541
permissions -rw-r--r--
removed axiom; added fact, dynamic_fact, prop;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/markup.ML
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     4
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     5
Common markup elements.
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     6
*)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     7
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     8
signature MARKUP =
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     9
sig
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    10
  type property = string * string
23658
wenzelm
parents: 23644
diff changeset
    11
  type T = string * property list
23794
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
    12
  val get_string: T -> string -> string option
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
    13
  val get_int: T -> string -> int option
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    14
  val none: T
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    15
  val properties: (string * string) list -> T -> T
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    16
  val nameN: string
25982
caee173104d3 added theorem group property;
wenzelm
parents: 25844
diff changeset
    17
  val groupN: string
26977
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
    18
  val theory_nameN: string
25808
c7aaa3f6f0ac added id property;
wenzelm
parents: 25552
diff changeset
    19
  val idN: string
23658
wenzelm
parents: 23644
diff changeset
    20
  val kindN: string
24777
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    21
  val internalK: string
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    22
  val property_internal: property
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    23
  val lineN: string
26001
d0a133941155 added column property;
wenzelm
parents: 25982
diff changeset
    24
  val columnN: string
27735
044901e02cc6 added end_line, end_column properties;
wenzelm
parents: 27660
diff changeset
    25
  val end_lineN: string
044901e02cc6 added end_line, end_column properties;
wenzelm
parents: 27660
diff changeset
    26
  val end_columnN: string
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    27
  val fileN: string
26051
43bcb30a6d97 added position_properties;
wenzelm
parents: 26001
diff changeset
    28
  val position_properties: string list
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    29
  val positionN: string val position: T
26255
2246d8bbe89d added location;
wenzelm
parents: 26051
diff changeset
    30
  val locationN: string val location: T
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
    31
  val indentN: string
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    32
  val blockN: string val block: int -> T
23695
6c4662bb4862 Add widthN to signature
aspinall
parents: 23671
diff changeset
    33
  val widthN: string
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
    34
  val breakN: string val break: int -> T
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
    35
  val fbreakN: string val fbreak: T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    36
  val classN: string val class: string -> T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    37
  val tyconN: string val tycon: string -> T
26702
a079f8f0080b added markup for fixed variables (local constants);
wenzelm
parents: 26255
diff changeset
    38
  val fixedN: string val fixed: string -> T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    39
  val constN: string val const: string -> T
27740
0b22524c05e2 removed axiom;
wenzelm
parents: 27735
diff changeset
    40
  val factN: string val fact: string -> T
0b22524c05e2 removed axiom;
wenzelm
parents: 27735
diff changeset
    41
  val dynamic_factN: string val dynamic_fact: string -> T
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    42
  val tfreeN: string val tfree: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    43
  val tvarN: string val tvar: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    44
  val freeN: string val free: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    45
  val skolemN: string val skolem: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    46
  val boundN: string val bound: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    47
  val varN: string val var: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    48
  val numN: string val num: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    49
  val xnumN: string val xnum: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    50
  val xstrN: string val xstr: T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    51
  val sortN: string val sort: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    52
  val typN: string val typ: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    53
  val termN: string val term: T
27740
0b22524c05e2 removed axiom;
wenzelm
parents: 27735
diff changeset
    54
  val propN: string val prop: T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    55
  val keywordN: string val keyword: string -> T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    56
  val commandN: string val command: string -> T
24870
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
    57
  val keyword_declN: string val keyword_decl: string -> T
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
    58
  val command_declN: string val command_decl: string -> string -> T
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    59
  val stringN: string val string: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    60
  val altstringN: string val altstring: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    61
  val verbatimN: string val verbatim: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    62
  val commentN: string val comment: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    63
  val controlN: string val control: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    64
  val malformedN: string val malformed: T
23786
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
    65
  val antiqN: string val antiq: T
27660
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
    66
  val command_spanN: string val command_span: string -> T
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
    67
  val ignored_spanN: string val ignored_span: T
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
    68
  val unknown_spanN: string val unknown_span: T
27523
56eb04c7b6b2 added prompt markup;
wenzelm
parents: 26977
diff changeset
    69
  val promptN: string val prompt: T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    70
  val stateN: string val state: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    71
  val subgoalN: string val subgoal: T
24289
bfd59eb6e24e added sendback;
wenzelm
parents: 23922
diff changeset
    72
  val sendbackN: string val sendback: T
24555
ea220faa69e7 added hilite markup;
wenzelm
parents: 24289
diff changeset
    73
  val hiliteN: string val hilite: T
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
    74
  val unprocessedN: string val unprocessed: T
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
    75
  val runningN: string val running: T
27615
wenzelm
parents: 27606
diff changeset
    76
  val failedN: string val failed: T
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
    77
  val finishedN: string val finished: T
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
    78
  val disposedN: string val disposed: T
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    79
  val default_output: T -> output * output
23786
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
    80
  val add_mode: string -> (T -> output * output) -> unit
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    81
  val output: T -> output * output
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    82
  val enclose: T -> output -> output
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
    83
  val markup: T -> string -> string
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    84
end;
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    85
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    86
structure Markup: MARKUP =
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    87
struct
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    88
23658
wenzelm
parents: 23644
diff changeset
    89
(* basic markup *)
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    90
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    91
type property = string * string;
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    92
type T = string * property list;
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    93
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    94
val none = ("", []);
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    95
23794
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
    96
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    97
fun properties more_props ((elem, props): T) =
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    98
  (elem, fold_rev (AList.update (op =)) more_props props);
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    99
23794
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
   100
fun get_string ((_, props): T) prop = AList.lookup (op =) props prop;
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
   101
fun get_int m prop = (case get_string m prop of NONE => NONE | SOME s => Int.fromString s);
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
   102
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   103
fun markup_elem elem = (elem, (elem, []): T);
23794
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
   104
fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
   105
fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
   106
26977
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
   107
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
   108
(* name *)
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
   109
23658
wenzelm
parents: 23644
diff changeset
   110
val nameN = "name";
25982
caee173104d3 added theorem group property;
wenzelm
parents: 25844
diff changeset
   111
val groupN = "group";
26977
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
   112
val theory_nameN = "theory_name";
24777
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   113
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   114
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   115
(* kind *)
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   116
23658
wenzelm
parents: 23644
diff changeset
   117
val kindN = "kind";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   118
24777
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   119
val internalK = "internal";
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   120
val property_internal = (kindN, internalK);
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   121
23658
wenzelm
parents: 23644
diff changeset
   122
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   123
(* position *)
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   124
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   125
val lineN = "line";
26001
d0a133941155 added column property;
wenzelm
parents: 25982
diff changeset
   126
val columnN = "column";
27735
044901e02cc6 added end_line, end_column properties;
wenzelm
parents: 27660
diff changeset
   127
val end_lineN = "end_line";
044901e02cc6 added end_line, end_column properties;
wenzelm
parents: 27660
diff changeset
   128
val end_columnN = "end_column";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   129
val fileN = "file";
25816
d2a94e6a7d1e moved id to position properties;
wenzelm
parents: 25808
diff changeset
   130
val idN = "id";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   131
27735
044901e02cc6 added end_line, end_column properties;
wenzelm
parents: 27660
diff changeset
   132
val position_properties = [lineN, columnN, end_lineN, end_columnN, fileN, idN];
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   133
val (positionN, position) = markup_elem "position";
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   134
26255
2246d8bbe89d added location;
wenzelm
parents: 26051
diff changeset
   135
val (locationN, location) = markup_elem "location";
2246d8bbe89d added location;
wenzelm
parents: 26051
diff changeset
   136
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   137
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   138
(* pretty printing *)
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   139
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   140
val indentN = "indent";
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   141
val (blockN, block) = markup_int "block" indentN;
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   142
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   143
val widthN = "width";
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   144
val (breakN, break) = markup_int "break" widthN;
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   145
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   146
val (fbreakN, fbreak) = markup_elem "fbreak";
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   147
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   148
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   149
(* logical entities *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   150
23658
wenzelm
parents: 23644
diff changeset
   151
val (classN, class) = markup_string "class" nameN;
wenzelm
parents: 23644
diff changeset
   152
val (tyconN, tycon) = markup_string "tycon" nameN;
26702
a079f8f0080b added markup for fixed variables (local constants);
wenzelm
parents: 26255
diff changeset
   153
val (fixedN, fixed) = markup_string "fixed" nameN;
23658
wenzelm
parents: 23644
diff changeset
   154
val (constN, const) = markup_string "const" nameN;
27740
0b22524c05e2 removed axiom;
wenzelm
parents: 27735
diff changeset
   155
val (factN, fact) = markup_string "fact" nameN;
0b22524c05e2 removed axiom;
wenzelm
parents: 27735
diff changeset
   156
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   157
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   158
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   159
(* inner syntax *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   160
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   161
val (tfreeN, tfree) = markup_elem "tfree";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   162
val (tvarN, tvar) = markup_elem "tvar";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   163
val (freeN, free) = markup_elem "free";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   164
val (skolemN, skolem) = markup_elem "skolem";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   165
val (boundN, bound) = markup_elem "bound";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   166
val (varN, var) = markup_elem "var";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   167
val (numN, num) = markup_elem "num";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   168
val (xnumN, xnum) = markup_elem "xnum";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   169
val (xstrN, xstr) = markup_elem "xstr";
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   170
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   171
val (sortN, sort) = markup_elem "sort";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   172
val (typN, typ) = markup_elem "typ";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   173
val (termN, term) = markup_elem "term";
27740
0b22524c05e2 removed axiom;
wenzelm
parents: 27735
diff changeset
   174
val (propN, prop) = markup_elem "prop";
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   175
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   176
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   177
(* outer syntax *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   178
23658
wenzelm
parents: 23644
diff changeset
   179
val (keywordN, keyword) = markup_string "keyword" nameN;
wenzelm
parents: 23644
diff changeset
   180
val (commandN, command) = markup_string "command" nameN;
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   181
24870
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   182
val (keyword_declN, keyword_decl) = markup_string "keyword_decl" nameN;
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   183
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   184
val command_declN = "command_decl";
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   185
fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   186
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   187
val (stringN, string) = markup_elem "string";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   188
val (altstringN, altstring) = markup_elem "altstring";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   189
val (verbatimN, verbatim) = markup_elem "verbatim";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   190
val (commentN, comment) = markup_elem "comment";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   191
val (controlN, control) = markup_elem "control";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   192
val (malformedN, malformed) = markup_elem "malformed";
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   193
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   194
val (antiqN, antiq) = markup_elem "antiq";
23786
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
   195
27660
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
   196
val (command_spanN, command_span) = markup_string "command_span" nameN;
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
   197
val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
   198
val (unknown_spanN, unknown_span) = markup_elem "unknown_span";
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   199
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   200
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   201
(* toplevel *)
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   202
27523
56eb04c7b6b2 added prompt markup;
wenzelm
parents: 26977
diff changeset
   203
val (promptN, prompt) = markup_elem "prompt";
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   204
val (stateN, state) = markup_elem "state";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   205
val (subgoalN, subgoal) = markup_elem "subgoal";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   206
val (sendbackN, sendback) = markup_elem "sendback";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   207
val (hiliteN, hilite) = markup_elem "hilite";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   208
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   209
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   210
(* command status *)
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   211
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   212
val (unprocessedN, unprocessed) = markup_elem "unprocessed";
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   213
val (runningN, running) = markup_elem "running";
27615
wenzelm
parents: 27606
diff changeset
   214
val (failedN, failed) = markup_elem "failed";
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   215
val (finishedN, finished) = markup_elem "finished";
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   216
val (disposedN, disposed) = markup_elem "disposed";
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   217
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   218
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   219
(* print mode operations *)
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   220
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   221
fun default_output (_: T) = ("", "");
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   222
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   223
local
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   224
  val default = {output = default_output};
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   225
  val modes = ref (Symtab.make [("", default)]);
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   226
in
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23794
diff changeset
   227
  fun add_mode name output = CRITICAL (fn () =>
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23794
diff changeset
   228
    change modes (Symtab.update_new (name, {output = output})));
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   229
  fun get_mode () =
24612
d1b315bdb8d7 avoid direct access to print_mode;
wenzelm
parents: 24555
diff changeset
   230
    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   231
end;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   232
23786
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
   233
fun output ("", _) = ("", "")
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
   234
  | output m = #output (get_mode ()) m;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   235
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   236
val enclose = output #-> Library.enclose;
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   237
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   238
fun markup m =
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   239
  let val (bg, en) = output m
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   240
  in Library.enclose (Output.escape bg) (Output.escape en) end;
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   241
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   242
end;