src/Pure/General/markup.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24777 c1250851d701
child 24870 9d057ff8e74c
permissions -rw-r--r--
filtering out some package theorems
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
23658
wenzelm
parents: 23644
diff changeset
    17
  val kindN: string
24777
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    18
  val internalK: string
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    19
  val property_internal: property
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    20
  val lineN: string
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    21
  val fileN: string
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    22
  val positionN: string val position: T
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
    23
  val indentN: string
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    24
  val blockN: string val block: int -> T
23695
6c4662bb4862 Add widthN to signature
aspinall
parents: 23671
diff changeset
    25
  val widthN: string
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
    26
  val breakN: string val break: int -> T
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
    27
  val fbreakN: string val fbreak: T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    28
  val classN: string val class: string -> T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    29
  val tyconN: string val tycon: string -> T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    30
  val constN: string val const: string -> T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    31
  val axiomN: string val axiom: string -> T
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    32
  val tfreeN: string val tfree: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    33
  val tvarN: string val tvar: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    34
  val freeN: string val free: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    35
  val skolemN: string val skolem: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    36
  val boundN: string val bound: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    37
  val varN: string val var: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    38
  val numN: string val num: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    39
  val xnumN: string val xnum: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    40
  val xstrN: string val xstr: T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    41
  val sortN: string val sort: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    42
  val typN: string val typ: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    43
  val termN: string val term: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    44
  val keywordN: string val keyword: string -> T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    45
  val commandN: string val command: string -> T
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    46
  val stringN: string val string: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    47
  val altstringN: string val altstring: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    48
  val verbatimN: string val verbatim: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    49
  val commentN: string val comment: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    50
  val controlN: string val control: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    51
  val malformedN: string val malformed: T
23786
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
    52
  val antiqN: string val antiq: T
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    53
  val whitespaceN: string val whitespace: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    54
  val junkN: string val junk: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    55
  val commandspanN: string val commandspan: string -> T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    56
  val promptN: string val prompt: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    57
  val stateN: string val state: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    58
  val subgoalN: string val subgoal: T
24289
bfd59eb6e24e added sendback;
wenzelm
parents: 23922
diff changeset
    59
  val sendbackN: string val sendback: T
24555
ea220faa69e7 added hilite markup;
wenzelm
parents: 24289
diff changeset
    60
  val hiliteN: string val hilite: T
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    61
  val default_output: T -> output * output
23786
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
    62
  val add_mode: string -> (T -> output * output) -> unit
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    63
  val output: T -> output * output
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    64
  val enclose: T -> output -> output
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    65
end;
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    66
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    67
structure Markup: MARKUP =
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    68
struct
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    69
23658
wenzelm
parents: 23644
diff changeset
    70
(* basic markup *)
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    71
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    72
type property = string * string;
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    73
type T = string * property list;
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    74
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    75
val none = ("", []);
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    76
23794
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
    77
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    78
fun properties more_props ((elem, props): T) =
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    79
  (elem, fold_rev (AList.update (op =)) more_props props);
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    80
23794
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
    81
fun get_string ((_, props): T) prop = AList.lookup (op =) props prop;
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
    82
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
    83
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
    84
fun markup elem = (elem, (elem, []): T);
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
    85
fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
    86
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
    87
23658
wenzelm
parents: 23644
diff changeset
    88
val nameN = "name";
24777
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    89
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    90
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    91
(* kind *)
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    92
23658
wenzelm
parents: 23644
diff changeset
    93
val kindN = "kind";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    94
24777
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    95
val internalK = "internal";
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    96
val property_internal = (kindN, internalK);
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    97
23658
wenzelm
parents: 23644
diff changeset
    98
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    99
(* position *)
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   100
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   101
val lineN = "line";
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   102
val fileN = "file";
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   103
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   104
val (positionN, position) = markup "position";
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   105
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   106
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   107
(* pretty printing *)
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   108
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   109
val indentN = "indent";
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   110
val (blockN, block) = markup_int "block" indentN;
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   111
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   112
val widthN = "width";
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   113
val (breakN, break) = markup_int "break" widthN;
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   114
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   115
val (fbreakN, fbreak) = markup "fbreak";
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   116
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   117
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   118
(* logical entities *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   119
23658
wenzelm
parents: 23644
diff changeset
   120
val (classN, class) = markup_string "class" nameN;
wenzelm
parents: 23644
diff changeset
   121
val (tyconN, tycon) = markup_string "tycon" nameN;
wenzelm
parents: 23644
diff changeset
   122
val (constN, const) = markup_string "const" nameN;
wenzelm
parents: 23644
diff changeset
   123
val (axiomN, axiom) = markup_string "axiom" nameN;
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   124
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   125
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   126
(* inner syntax *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   127
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   128
val (tfreeN, tfree) = markup "tfree";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   129
val (tvarN, tvar) = markup "tvar";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   130
val (freeN, free) = markup "free";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   131
val (skolemN, skolem) = markup "skolem";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   132
val (boundN, bound) = markup "bound";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   133
val (varN, var) = markup "var";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   134
val (numN, num) = markup "num";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   135
val (xnumN, xnum) = markup "xnum";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   136
val (xstrN, xstr) = markup "xstr";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   137
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   138
val (sortN, sort) = markup "sort";
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   139
val (typN, typ) = markup "typ";
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   140
val (termN, term) = markup "term";
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   141
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   142
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   143
(* outer syntax *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   144
23658
wenzelm
parents: 23644
diff changeset
   145
val (keywordN, keyword) = markup_string "keyword" nameN;
wenzelm
parents: 23644
diff changeset
   146
val (commandN, command) = markup_string "command" nameN;
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   147
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   148
val (stringN, string) = markup "string";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   149
val (altstringN, altstring) = markup "altstring";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   150
val (verbatimN, verbatim) = markup "verbatim";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   151
val (commentN, comment) = markup "comment";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   152
val (controlN, control) = markup "control";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   153
val (malformedN, malformed) = markup "malformed";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   154
23786
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
   155
val (antiqN, antiq) = markup "antiq";
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
   156
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   157
val (whitespaceN, whitespace) = markup "whitespace";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   158
val (junkN, junk) = markup "junk";
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   159
val (commandspanN, commandspan) = markup_string "commandspan" nameN;
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   160
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   161
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   162
(* toplevel *)
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   163
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   164
val (promptN, prompt) = markup "prompt";
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   165
val (stateN, state) = markup "state";
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   166
val (subgoalN, subgoal) = markup "subgoal";
24289
bfd59eb6e24e added sendback;
wenzelm
parents: 23922
diff changeset
   167
val (sendbackN, sendback) = markup "sendback";
24555
ea220faa69e7 added hilite markup;
wenzelm
parents: 24289
diff changeset
   168
val (hiliteN, hilite) = markup "hilite";
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   169
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   170
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   171
(* print mode operations *)
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   172
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   173
fun default_output (_: T) = ("", "");
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   174
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   175
local
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   176
  val default = {output = default_output};
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   177
  val modes = ref (Symtab.make [("", default)]);
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   178
in
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23794
diff changeset
   179
  fun add_mode name output = CRITICAL (fn () =>
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23794
diff changeset
   180
    change modes (Symtab.update_new (name, {output = output})));
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   181
  fun get_mode () =
24612
d1b315bdb8d7 avoid direct access to print_mode;
wenzelm
parents: 24555
diff changeset
   182
    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   183
end;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   184
23786
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
   185
fun output ("", _) = ("", "")
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
   186
  | output m = #output (get_mode ()) m;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   187
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   188
val enclose = output #-> Library.enclose;
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   189
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   190
end;