src/Pure/General/markup.ML
author wenzelm
Thu Apr 03 18:42:36 2008 +0200 (2008-04-03)
changeset 26538 d65504ffb47d
parent 26255 2246d8bbe89d
child 26702 a079f8f0080b
permissions -rw-r--r--
replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm@23623
     1
(*  Title:      Pure/General/markup.ML
wenzelm@23623
     2
    ID:         $Id$
wenzelm@23623
     3
    Author:     Makarius
wenzelm@23623
     4
wenzelm@23623
     5
Common markup elements.
wenzelm@23623
     6
*)
wenzelm@23623
     7
wenzelm@23623
     8
signature MARKUP =
wenzelm@23623
     9
sig
wenzelm@23623
    10
  type property = string * string
wenzelm@23658
    11
  type T = string * property list
wenzelm@23794
    12
  val get_string: T -> string -> string option
wenzelm@23794
    13
  val get_int: T -> string -> int option
wenzelm@23704
    14
  val none: T
wenzelm@23704
    15
  val properties: (string * string) list -> T -> T
wenzelm@23623
    16
  val nameN: string
wenzelm@25982
    17
  val groupN: string
wenzelm@25808
    18
  val idN: string
wenzelm@23658
    19
  val kindN: string
wenzelm@24777
    20
  val internalK: string
wenzelm@24777
    21
  val property_internal: property
wenzelm@23671
    22
  val lineN: string
wenzelm@26001
    23
  val columnN: string
wenzelm@23671
    24
  val fileN: string
wenzelm@26051
    25
  val position_properties: string list
wenzelm@23671
    26
  val positionN: string val position: T
wenzelm@26255
    27
  val locationN: string val location: T
wenzelm@23644
    28
  val indentN: string
wenzelm@23704
    29
  val blockN: string val block: int -> T
aspinall@23695
    30
  val widthN: string
wenzelm@23644
    31
  val breakN: string val break: int -> T
wenzelm@23644
    32
  val fbreakN: string val fbreak: T
wenzelm@23637
    33
  val classN: string val class: string -> T
wenzelm@23637
    34
  val tyconN: string val tycon: string -> T
wenzelm@23637
    35
  val constN: string val const: string -> T
wenzelm@23637
    36
  val axiomN: string val axiom: string -> T
wenzelm@23719
    37
  val tfreeN: string val tfree: T
wenzelm@23719
    38
  val tvarN: string val tvar: T
wenzelm@23719
    39
  val freeN: string val free: T
wenzelm@23719
    40
  val skolemN: string val skolem: T
wenzelm@23719
    41
  val boundN: string val bound: T
wenzelm@23719
    42
  val varN: string val var: T
wenzelm@23719
    43
  val numN: string val num: T
wenzelm@23719
    44
  val xnumN: string val xnum: T
wenzelm@23719
    45
  val xstrN: string val xstr: T
wenzelm@23637
    46
  val sortN: string val sort: T
wenzelm@23637
    47
  val typN: string val typ: T
wenzelm@23637
    48
  val termN: string val term: T
wenzelm@23637
    49
  val keywordN: string val keyword: string -> T
wenzelm@23637
    50
  val commandN: string val command: string -> T
wenzelm@24870
    51
  val keyword_declN: string val keyword_decl: string -> T
wenzelm@24870
    52
  val command_declN: string val command_decl: string -> string -> T
wenzelm@23719
    53
  val stringN: string val string: T
wenzelm@23719
    54
  val altstringN: string val altstring: T
wenzelm@23719
    55
  val verbatimN: string val verbatim: T
wenzelm@23719
    56
  val commentN: string val comment: T
wenzelm@23719
    57
  val controlN: string val control: T
wenzelm@23719
    58
  val malformedN: string val malformed: T
wenzelm@23786
    59
  val antiqN: string val antiq: T
wenzelm@23719
    60
  val whitespaceN: string val whitespace: T
wenzelm@23719
    61
  val junkN: string val junk: T
wenzelm@23719
    62
  val commandspanN: string val commandspan: string -> T
wenzelm@23637
    63
  val stateN: string val state: T
wenzelm@23637
    64
  val subgoalN: string val subgoal: T
wenzelm@24289
    65
  val sendbackN: string val sendback: T
wenzelm@24555
    66
  val hiliteN: string val hilite: T
wenzelm@23704
    67
  val default_output: T -> output * output
wenzelm@23786
    68
  val add_mode: string -> (T -> output * output) -> unit
wenzelm@23704
    69
  val output: T -> output * output
wenzelm@23719
    70
  val enclose: T -> output -> output
wenzelm@25552
    71
  val markup: T -> string -> string
wenzelm@23623
    72
end;
wenzelm@23623
    73
wenzelm@23623
    74
structure Markup: MARKUP =
wenzelm@23623
    75
struct
wenzelm@23623
    76
wenzelm@23658
    77
(* basic markup *)
wenzelm@23623
    78
wenzelm@23637
    79
type property = string * string;
wenzelm@23637
    80
type T = string * property list;
wenzelm@23637
    81
wenzelm@23637
    82
val none = ("", []);
wenzelm@23637
    83
wenzelm@23794
    84
wenzelm@23671
    85
fun properties more_props ((elem, props): T) =
wenzelm@23671
    86
  (elem, fold_rev (AList.update (op =)) more_props props);
wenzelm@23671
    87
wenzelm@23794
    88
fun get_string ((_, props): T) prop = AList.lookup (op =) props prop;
wenzelm@23794
    89
fun get_int m prop = (case get_string m prop of NONE => NONE | SOME s => Int.fromString s);
wenzelm@23794
    90
wenzelm@25552
    91
fun markup_elem elem = (elem, (elem, []): T);
wenzelm@23794
    92
fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
wenzelm@23794
    93
fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
wenzelm@23794
    94
wenzelm@23658
    95
val nameN = "name";
wenzelm@25982
    96
val groupN = "group";
wenzelm@24777
    97
wenzelm@24777
    98
wenzelm@24777
    99
(* kind *)
wenzelm@24777
   100
wenzelm@23658
   101
val kindN = "kind";
wenzelm@23671
   102
wenzelm@24777
   103
val internalK = "internal";
wenzelm@24777
   104
val property_internal = (kindN, internalK);
wenzelm@24777
   105
wenzelm@23658
   106
wenzelm@23671
   107
(* position *)
wenzelm@23671
   108
wenzelm@23671
   109
val lineN = "line";
wenzelm@26001
   110
val columnN = "column";
wenzelm@23671
   111
val fileN = "file";
wenzelm@25816
   112
val idN = "id";
wenzelm@23671
   113
wenzelm@26051
   114
val position_properties = [lineN, columnN, fileN, idN];
wenzelm@25552
   115
val (positionN, position) = markup_elem "position";
wenzelm@23644
   116
wenzelm@26255
   117
val (locationN, location) = markup_elem "location";
wenzelm@26255
   118
wenzelm@23644
   119
wenzelm@23644
   120
(* pretty printing *)
wenzelm@23644
   121
wenzelm@23644
   122
val indentN = "indent";
wenzelm@23644
   123
val (blockN, block) = markup_int "block" indentN;
wenzelm@23644
   124
wenzelm@23644
   125
val widthN = "width";
wenzelm@23644
   126
val (breakN, break) = markup_int "break" widthN;
wenzelm@23644
   127
wenzelm@25552
   128
val (fbreakN, fbreak) = markup_elem "fbreak";
wenzelm@23637
   129
wenzelm@23637
   130
wenzelm@23623
   131
(* logical entities *)
wenzelm@23623
   132
wenzelm@23658
   133
val (classN, class) = markup_string "class" nameN;
wenzelm@23658
   134
val (tyconN, tycon) = markup_string "tycon" nameN;
wenzelm@23658
   135
val (constN, const) = markup_string "const" nameN;
wenzelm@23658
   136
val (axiomN, axiom) = markup_string "axiom" nameN;
wenzelm@23623
   137
wenzelm@23623
   138
wenzelm@23623
   139
(* inner syntax *)
wenzelm@23623
   140
wenzelm@25552
   141
val (tfreeN, tfree) = markup_elem "tfree";
wenzelm@25552
   142
val (tvarN, tvar) = markup_elem "tvar";
wenzelm@25552
   143
val (freeN, free) = markup_elem "free";
wenzelm@25552
   144
val (skolemN, skolem) = markup_elem "skolem";
wenzelm@25552
   145
val (boundN, bound) = markup_elem "bound";
wenzelm@25552
   146
val (varN, var) = markup_elem "var";
wenzelm@25552
   147
val (numN, num) = markup_elem "num";
wenzelm@25552
   148
val (xnumN, xnum) = markup_elem "xnum";
wenzelm@25552
   149
val (xstrN, xstr) = markup_elem "xstr";
wenzelm@23719
   150
wenzelm@25552
   151
val (sortN, sort) = markup_elem "sort";
wenzelm@25552
   152
val (typN, typ) = markup_elem "typ";
wenzelm@25552
   153
val (termN, term) = markup_elem "term";
wenzelm@23623
   154
wenzelm@23623
   155
wenzelm@23623
   156
(* outer syntax *)
wenzelm@23623
   157
wenzelm@23658
   158
val (keywordN, keyword) = markup_string "keyword" nameN;
wenzelm@23658
   159
val (commandN, command) = markup_string "command" nameN;
wenzelm@23637
   160
wenzelm@24870
   161
val (keyword_declN, keyword_decl) = markup_string "keyword_decl" nameN;
wenzelm@24870
   162
wenzelm@24870
   163
val command_declN = "command_decl";
wenzelm@24870
   164
fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
wenzelm@24870
   165
wenzelm@25552
   166
val (stringN, string) = markup_elem "string";
wenzelm@25552
   167
val (altstringN, altstring) = markup_elem "altstring";
wenzelm@25552
   168
val (verbatimN, verbatim) = markup_elem "verbatim";
wenzelm@25552
   169
val (commentN, comment) = markup_elem "comment";
wenzelm@25552
   170
val (controlN, control) = markup_elem "control";
wenzelm@25552
   171
val (malformedN, malformed) = markup_elem "malformed";
wenzelm@23719
   172
wenzelm@25552
   173
val (antiqN, antiq) = markup_elem "antiq";
wenzelm@23786
   174
wenzelm@25552
   175
val (whitespaceN, whitespace) = markup_elem "whitespace";
wenzelm@25552
   176
val (junkN, junk) = markup_elem "junk";
wenzelm@23719
   177
val (commandspanN, commandspan) = markup_string "commandspan" nameN;
wenzelm@23719
   178
wenzelm@23623
   179
wenzelm@23637
   180
(* toplevel *)
wenzelm@23637
   181
wenzelm@25552
   182
val (stateN, state) = markup_elem "state";
wenzelm@25552
   183
val (subgoalN, subgoal) = markup_elem "subgoal";
wenzelm@25552
   184
val (sendbackN, sendback) = markup_elem "sendback";
wenzelm@25552
   185
val (hiliteN, hilite) = markup_elem "hilite";
wenzelm@25552
   186
wenzelm@25552
   187
wenzelm@23704
   188
(* print mode operations *)
wenzelm@23704
   189
wenzelm@23704
   190
fun default_output (_: T) = ("", "");
wenzelm@23704
   191
wenzelm@23704
   192
local
wenzelm@23704
   193
  val default = {output = default_output};
wenzelm@23704
   194
  val modes = ref (Symtab.make [("", default)]);
wenzelm@23704
   195
in
wenzelm@23922
   196
  fun add_mode name output = CRITICAL (fn () =>
wenzelm@23922
   197
    change modes (Symtab.update_new (name, {output = output})));
wenzelm@23704
   198
  fun get_mode () =
wenzelm@24612
   199
    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
wenzelm@23623
   200
end;
wenzelm@23704
   201
wenzelm@23786
   202
fun output ("", _) = ("", "")
wenzelm@23786
   203
  | output m = #output (get_mode ()) m;
wenzelm@23704
   204
wenzelm@23719
   205
val enclose = output #-> Library.enclose;
wenzelm@23719
   206
wenzelm@25552
   207
fun markup m =
wenzelm@25552
   208
  let val (bg, en) = output m
wenzelm@25552
   209
  in Library.enclose (Output.escape bg) (Output.escape en) end;
wenzelm@25552
   210
wenzelm@23704
   211
end;