src/Pure/General/markup.ML
author wenzelm
Sun Apr 17 21:17:45 2011 +0200 (2011-04-17)
changeset 42380 9371ea9f91fb
parent 42378 d9fe47d21b41
child 42492 83c57d850049
permissions -rw-r--r--
markup attributes/methods via name space;
eliminated obsolete markup;
wenzelm@23623
     1
(*  Title:      Pure/General/markup.ML
wenzelm@23623
     2
    Author:     Makarius
wenzelm@23623
     3
wenzelm@23623
     4
Common markup elements.
wenzelm@23623
     5
*)
wenzelm@23623
     6
wenzelm@23623
     7
signature MARKUP =
wenzelm@23623
     8
sig
wenzelm@38414
     9
  val parse_int: string -> int
wenzelm@38414
    10
  val print_int: int -> string
wenzelm@28017
    11
  type T = string * Properties.T
wenzelm@38474
    12
  val empty: T
wenzelm@38474
    13
  val is_empty: T -> bool
wenzelm@38229
    14
  val properties: Properties.T -> T -> T
wenzelm@23623
    15
  val nameN: string
wenzelm@27818
    16
  val name: string -> T -> T
wenzelm@38887
    17
  val kindN: string
wenzelm@30221
    18
  val bindingN: string val binding: string -> T
wenzelm@42135
    19
  val entityN: string val entity: string -> string -> T
wenzelm@33088
    20
  val defN: string
wenzelm@33088
    21
  val refN: string
wenzelm@23671
    22
  val lineN: string
wenzelm@26001
    23
  val columnN: string
wenzelm@27794
    24
  val offsetN: string
wenzelm@27794
    25
  val end_offsetN: string
wenzelm@23671
    26
  val fileN: string
wenzelm@30221
    27
  val idN: string
wenzelm@27748
    28
  val position_properties': string list
wenzelm@26051
    29
  val position_properties: string list
wenzelm@23671
    30
  val positionN: string val position: T
wenzelm@23644
    31
  val indentN: string
wenzelm@23704
    32
  val blockN: string val block: int -> T
aspinall@23695
    33
  val widthN: string
wenzelm@23644
    34
  val breakN: string val break: int -> T
wenzelm@23644
    35
  val fbreakN: string val fbreak: T
wenzelm@33985
    36
  val hiddenN: string val hidden: T
wenzelm@27828
    37
  val tclassN: string val tclass: string -> T
wenzelm@23637
    38
  val tyconN: string val tycon: string -> T
wenzelm@28077
    39
  val fixed_declN: string val fixed_decl: string -> T
wenzelm@26702
    40
  val fixedN: string val fixed: string -> T
wenzelm@23637
    41
  val constN: string val const: string -> T
wenzelm@27740
    42
  val dynamic_factN: string val dynamic_fact: string -> T
wenzelm@23719
    43
  val tfreeN: string val tfree: T
wenzelm@23719
    44
  val tvarN: string val tvar: T
wenzelm@23719
    45
  val freeN: string val free: T
wenzelm@23719
    46
  val skolemN: string val skolem: T
wenzelm@23719
    47
  val boundN: string val bound: T
wenzelm@23719
    48
  val varN: string val var: T
wenzelm@29318
    49
  val numeralN: string val numeral: T
wenzelm@27804
    50
  val literalN: string val literal: T
wenzelm@29318
    51
  val inner_stringN: string val inner_string: T
wenzelm@27883
    52
  val inner_commentN: string val inner_comment: T
wenzelm@39168
    53
  val token_rangeN: string val token_range: T
wenzelm@23637
    54
  val sortN: string val sort: T
wenzelm@23637
    55
  val typN: string val typ: T
wenzelm@23637
    56
  val termN: string val term: T
wenzelm@27818
    57
  val propN: string val prop: T
wenzelm@30614
    58
  val ML_keywordN: string val ML_keyword: T
wenzelm@37195
    59
  val ML_delimiterN: string val ML_delimiter: T
wenzelm@30614
    60
  val ML_identN: string val ML_ident: T
wenzelm@30614
    61
  val ML_tvarN: string val ML_tvar: T
wenzelm@30614
    62
  val ML_numeralN: string val ML_numeral: T
wenzelm@30614
    63
  val ML_charN: string val ML_char: T
wenzelm@30614
    64
  val ML_stringN: string val ML_string: T
wenzelm@30614
    65
  val ML_commentN: string val ML_comment: T
wenzelm@30614
    66
  val ML_malformedN: string val ML_malformed: T
wenzelm@42327
    67
  val ML_defN: string
wenzelm@42327
    68
  val ML_openN: string
wenzelm@42327
    69
  val ML_structN: string
wenzelm@30702
    70
  val ML_typingN: string val ML_typing: T
wenzelm@27875
    71
  val ML_sourceN: string val ML_source: T
wenzelm@27875
    72
  val doc_sourceN: string val doc_source: T
wenzelm@27879
    73
  val antiqN: string val antiq: T
wenzelm@27894
    74
  val ML_antiqN: string val ML_antiq: string -> T
wenzelm@27894
    75
  val doc_antiqN: string val doc_antiq: string -> T
wenzelm@27836
    76
  val keyword_declN: string val keyword_decl: string -> T
wenzelm@27836
    77
  val command_declN: string val command_decl: string -> string -> T
wenzelm@37193
    78
  val keywordN: string val keyword: T
wenzelm@37192
    79
  val operatorN: string val operator: T
wenzelm@37193
    80
  val commandN: string val command: T
wenzelm@27836
    81
  val identN: string val ident: T
wenzelm@23719
    82
  val stringN: string val string: T
wenzelm@23719
    83
  val altstringN: string val altstring: T
wenzelm@23719
    84
  val verbatimN: string val verbatim: T
wenzelm@23719
    85
  val commentN: string val comment: T
wenzelm@23719
    86
  val controlN: string val control: T
wenzelm@23719
    87
  val malformedN: string val malformed: T
wenzelm@38229
    88
  val tokenN: string val token: Properties.T -> T
wenzelm@27660
    89
  val command_spanN: string val command_span: string -> T
wenzelm@27660
    90
  val ignored_spanN: string val ignored_span: T
wenzelm@27836
    91
  val malformed_spanN: string val malformed_span: T
wenzelm@40394
    92
  val elapsedN: string
wenzelm@40394
    93
  val cpuN: string
wenzelm@40394
    94
  val gcN: string
wenzelm@42012
    95
  val timingN: string val timing: Timing.timing -> T
wenzelm@38721
    96
  val subgoalsN: string
wenzelm@38721
    97
  val proof_stateN: string val proof_state: int -> T
wenzelm@23637
    98
  val stateN: string val state: T
wenzelm@23637
    99
  val subgoalN: string val subgoal: T
wenzelm@24289
   100
  val sendbackN: string val sendback: T
wenzelm@24555
   101
  val hiliteN: string val hilite: T
wenzelm@29417
   102
  val taskN: string
wenzelm@37186
   103
  val forkedN: string val forked: T
wenzelm@37186
   104
  val joinedN: string val joined: T
wenzelm@27615
   105
  val failedN: string val failed: T
wenzelm@27606
   106
  val finishedN: string val finished: T
wenzelm@38414
   107
  val versionN: string
wenzelm@38414
   108
  val execN: string
wenzelm@38414
   109
  val assignN: string val assign: int -> T
wenzelm@38414
   110
  val editN: string val edit: int -> int -> T
wenzelm@38871
   111
  val serialN: string
wenzelm@27969
   112
  val promptN: string val prompt: T
wenzelm@31384
   113
  val readyN: string val ready: T
wenzelm@38887
   114
  val reportN: string val report: T
wenzelm@39439
   115
  val no_reportN: string val no_report: T
wenzelm@39171
   116
  val badN: string val bad: T
wenzelm@40131
   117
  val no_output: Output.output * Output.output
wenzelm@40131
   118
  val default_output: T -> Output.output * Output.output
wenzelm@40131
   119
  val add_mode: string -> (T -> Output.output * Output.output) -> unit
wenzelm@40131
   120
  val output: T -> Output.output * Output.output
wenzelm@40131
   121
  val enclose: T -> Output.output -> Output.output
wenzelm@25552
   122
  val markup: T -> string -> string
wenzelm@23623
   123
end;
wenzelm@23623
   124
wenzelm@23623
   125
structure Markup: MARKUP =
wenzelm@23623
   126
struct
wenzelm@23623
   127
wenzelm@30221
   128
(** markup elements **)
wenzelm@30221
   129
wenzelm@38414
   130
(* integers *)
wenzelm@38414
   131
wenzelm@38414
   132
fun parse_int s =
wenzelm@38414
   133
  (case Int.fromString s of
wenzelm@38414
   134
    SOME i => i
wenzelm@38414
   135
  | NONE => raise Fail ("Bad integer: " ^ quote s));
wenzelm@38414
   136
wenzelm@38414
   137
val print_int = signed_string_of_int;
wenzelm@38414
   138
wenzelm@38414
   139
wenzelm@23658
   140
(* basic markup *)
wenzelm@23623
   141
wenzelm@28017
   142
type T = string * Properties.T;
wenzelm@23637
   143
wenzelm@38474
   144
val empty = ("", []);
wenzelm@23637
   145
wenzelm@38474
   146
fun is_empty ("", _) = true
wenzelm@38474
   147
  | is_empty _ = false;
wenzelm@27883
   148
wenzelm@23794
   149
wenzelm@23671
   150
fun properties more_props ((elem, props): T) =
wenzelm@28017
   151
  (elem, fold_rev Properties.put more_props props);
wenzelm@23671
   152
wenzelm@25552
   153
fun markup_elem elem = (elem, (elem, []): T);
wenzelm@23794
   154
fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
wenzelm@38414
   155
fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
wenzelm@23794
   156
wenzelm@26977
   157
wenzelm@38721
   158
(* misc properties *)
wenzelm@26977
   159
wenzelm@23658
   160
val nameN = "name";
wenzelm@27818
   161
fun name a = properties [(nameN, a)];
wenzelm@27818
   162
wenzelm@23658
   163
val kindN = "kind";
wenzelm@23671
   164
wenzelm@23658
   165
wenzelm@33088
   166
(* formal entities *)
wenzelm@33088
   167
wenzelm@38887
   168
val (bindingN, binding) = markup_string "binding" nameN;
wenzelm@42135
   169
wenzelm@42135
   170
val entityN = "entity";
wenzelm@42377
   171
fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
wenzelm@33088
   172
wenzelm@33088
   173
val defN = "def";
wenzelm@33088
   174
val refN = "ref";
wenzelm@33088
   175
wenzelm@33088
   176
wenzelm@23671
   177
(* position *)
wenzelm@23671
   178
wenzelm@23671
   179
val lineN = "line";
wenzelm@26001
   180
val columnN = "column";
wenzelm@27794
   181
val offsetN = "offset";
wenzelm@27794
   182
val end_offsetN = "end_offset";
wenzelm@23671
   183
val fileN = "file";
wenzelm@25816
   184
val idN = "id";
wenzelm@23671
   185
wenzelm@41484
   186
val position_properties' = [fileN, idN];
wenzelm@41484
   187
val position_properties = [lineN, columnN, offsetN, end_offsetN] @ position_properties';
wenzelm@27748
   188
wenzelm@25552
   189
val (positionN, position) = markup_elem "position";
wenzelm@26255
   190
wenzelm@23644
   191
wenzelm@23644
   192
(* pretty printing *)
wenzelm@23644
   193
wenzelm@23644
   194
val indentN = "indent";
wenzelm@23644
   195
val (blockN, block) = markup_int "block" indentN;
wenzelm@23644
   196
wenzelm@23644
   197
val widthN = "width";
wenzelm@23644
   198
val (breakN, break) = markup_int "break" widthN;
wenzelm@23644
   199
wenzelm@25552
   200
val (fbreakN, fbreak) = markup_elem "fbreak";
wenzelm@23637
   201
wenzelm@23637
   202
wenzelm@33985
   203
(* hidden text *)
wenzelm@33985
   204
wenzelm@33985
   205
val (hiddenN, hidden) = markup_elem "hidden";
wenzelm@33985
   206
wenzelm@33985
   207
wenzelm@23623
   208
(* logical entities *)
wenzelm@23623
   209
wenzelm@27828
   210
val (tclassN, tclass) = markup_string "tclass" nameN;
wenzelm@23658
   211
val (tyconN, tycon) = markup_string "tycon" nameN;
wenzelm@28077
   212
val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN;
wenzelm@26702
   213
val (fixedN, fixed) = markup_string "fixed" nameN;
wenzelm@42135
   214
val (constN, const) = markup_string "constant" nameN;
wenzelm@27740
   215
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
wenzelm@23623
   216
wenzelm@23623
   217
wenzelm@23623
   218
(* inner syntax *)
wenzelm@23623
   219
wenzelm@25552
   220
val (tfreeN, tfree) = markup_elem "tfree";
wenzelm@25552
   221
val (tvarN, tvar) = markup_elem "tvar";
wenzelm@25552
   222
val (freeN, free) = markup_elem "free";
wenzelm@25552
   223
val (skolemN, skolem) = markup_elem "skolem";
wenzelm@25552
   224
val (boundN, bound) = markup_elem "bound";
wenzelm@25552
   225
val (varN, var) = markup_elem "var";
wenzelm@29318
   226
val (numeralN, numeral) = markup_elem "numeral";
wenzelm@27804
   227
val (literalN, literal) = markup_elem "literal";
wenzelm@29318
   228
val (inner_stringN, inner_string) = markup_elem "inner_string";
wenzelm@27883
   229
val (inner_commentN, inner_comment) = markup_elem "inner_comment";
wenzelm@23719
   230
wenzelm@39168
   231
val (token_rangeN, token_range) = markup_elem "token_range";
wenzelm@39168
   232
wenzelm@25552
   233
val (sortN, sort) = markup_elem "sort";
wenzelm@25552
   234
val (typN, typ) = markup_elem "typ";
wenzelm@25552
   235
val (termN, term) = markup_elem "term";
wenzelm@27818
   236
val (propN, prop) = markup_elem "prop";
wenzelm@27748
   237
wenzelm@23623
   238
wenzelm@30614
   239
(* ML syntax *)
wenzelm@30614
   240
wenzelm@30614
   241
val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
wenzelm@37195
   242
val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
wenzelm@30614
   243
val (ML_identN, ML_ident) = markup_elem "ML_ident";
wenzelm@30614
   244
val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
wenzelm@30614
   245
val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
wenzelm@30614
   246
val (ML_charN, ML_char) = markup_elem "ML_char";
wenzelm@30614
   247
val (ML_stringN, ML_string) = markup_elem "ML_string";
wenzelm@30614
   248
val (ML_commentN, ML_comment) = markup_elem "ML_comment";
wenzelm@30614
   249
val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
wenzelm@30614
   250
wenzelm@42327
   251
val ML_defN = "ML_def";
wenzelm@42327
   252
val ML_openN = "ML_open";
wenzelm@42327
   253
val ML_structN = "ML_struct";
wenzelm@30702
   254
val (ML_typingN, ML_typing) = markup_elem "ML_typing";
wenzelm@30702
   255
wenzelm@30614
   256
wenzelm@27875
   257
(* embedded source text *)
wenzelm@27875
   258
wenzelm@27875
   259
val (ML_sourceN, ML_source) = markup_elem "ML_source";
wenzelm@27875
   260
val (doc_sourceN, doc_source) = markup_elem "doc_source";
wenzelm@27875
   261
wenzelm@27879
   262
val (antiqN, antiq) = markup_elem "antiq";
wenzelm@27894
   263
val (ML_antiqN, ML_antiq) = markup_string "ML_antiq" nameN;
wenzelm@27894
   264
val (doc_antiqN, doc_antiq) = markup_string "doc_antiq" nameN;
wenzelm@27879
   265
wenzelm@27875
   266
wenzelm@23623
   267
(* outer syntax *)
wenzelm@23623
   268
wenzelm@24870
   269
val (keyword_declN, keyword_decl) = markup_string "keyword_decl" nameN;
wenzelm@24870
   270
wenzelm@24870
   271
val command_declN = "command_decl";
wenzelm@24870
   272
fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
wenzelm@24870
   273
wenzelm@37193
   274
val (keywordN, keyword) = markup_elem "keyword";
wenzelm@37192
   275
val (operatorN, operator) = markup_elem "operator";
wenzelm@37193
   276
val (commandN, command) = markup_elem "command";
wenzelm@27836
   277
val (identN, ident) = markup_elem "ident";
wenzelm@25552
   278
val (stringN, string) = markup_elem "string";
wenzelm@25552
   279
val (altstringN, altstring) = markup_elem "altstring";
wenzelm@25552
   280
val (verbatimN, verbatim) = markup_elem "verbatim";
wenzelm@25552
   281
val (commentN, comment) = markup_elem "comment";
wenzelm@25552
   282
val (controlN, control) = markup_elem "control";
wenzelm@25552
   283
val (malformedN, malformed) = markup_elem "malformed";
wenzelm@23719
   284
wenzelm@38229
   285
val tokenN = "token";
wenzelm@38229
   286
fun token props = (tokenN, props);
wenzelm@27851
   287
wenzelm@27660
   288
val (command_spanN, command_span) = markup_string "command_span" nameN;
wenzelm@27660
   289
val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
wenzelm@27836
   290
val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
wenzelm@23719
   291
wenzelm@23623
   292
wenzelm@40394
   293
(* timing *)
wenzelm@40394
   294
wenzelm@40394
   295
val timingN = "timing";
wenzelm@40394
   296
val elapsedN = "elapsed";
wenzelm@40394
   297
val cpuN = "cpu";
wenzelm@40394
   298
val gcN = "gc";
wenzelm@23637
   299
wenzelm@42012
   300
fun timing {elapsed, cpu, gc} =
wenzelm@40394
   301
  (timingN,
wenzelm@40394
   302
   [(elapsedN, Time.toString elapsed),
wenzelm@40394
   303
    (cpuN, Time.toString cpu),
wenzelm@40394
   304
    (gcN, Time.toString gc)]);
wenzelm@40394
   305
wenzelm@40394
   306
wenzelm@40394
   307
(* toplevel *)
wenzelm@40391
   308
wenzelm@38721
   309
val subgoalsN = "subgoals";
wenzelm@38721
   310
val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
wenzelm@38721
   311
wenzelm@25552
   312
val (stateN, state) = markup_elem "state";
wenzelm@25552
   313
val (subgoalN, subgoal) = markup_elem "subgoal";
wenzelm@25552
   314
val (sendbackN, sendback) = markup_elem "sendback";
wenzelm@25552
   315
val (hiliteN, hilite) = markup_elem "hilite";
wenzelm@25552
   316
wenzelm@25552
   317
wenzelm@27606
   318
(* command status *)
wenzelm@27606
   319
wenzelm@29417
   320
val taskN = "task";
wenzelm@29417
   321
wenzelm@37186
   322
val (forkedN, forked) = markup_elem "forked";
wenzelm@37186
   323
val (joinedN, joined) = markup_elem "joined";
wenzelm@38429
   324
wenzelm@27615
   325
val (failedN, failed) = markup_elem "failed";
wenzelm@27606
   326
val (finishedN, finished) = markup_elem "finished";
wenzelm@27606
   327
wenzelm@29488
   328
wenzelm@29488
   329
(* interactive documents *)
wenzelm@29488
   330
wenzelm@38414
   331
val versionN = "version";
wenzelm@38414
   332
val execN = "exec";
wenzelm@38414
   333
val (assignN, assign) = markup_int "assign" versionN;
wenzelm@34242
   334
wenzelm@29488
   335
val editN = "edit";
wenzelm@38414
   336
fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
wenzelm@29482
   337
wenzelm@27606
   338
wenzelm@27969
   339
(* messages *)
wenzelm@27969
   340
wenzelm@38871
   341
val serialN = "serial";
wenzelm@27969
   342
wenzelm@27969
   343
val (promptN, prompt) = markup_elem "prompt";
wenzelm@31384
   344
val (readyN, ready) = markup_elem "ready";
wenzelm@27969
   345
wenzelm@38887
   346
val (reportN, report) = markup_elem "report";
wenzelm@39439
   347
val (no_reportN, no_report) = markup_elem "no_report";
wenzelm@38887
   348
wenzelm@39171
   349
val (badN, bad) = markup_elem "bad";
wenzelm@39171
   350
wenzelm@27969
   351
wenzelm@27969
   352
wenzelm@30221
   353
(** print mode operations **)
wenzelm@23704
   354
wenzelm@29325
   355
val no_output = ("", "");
wenzelm@29325
   356
fun default_output (_: T) = no_output;
wenzelm@23704
   357
wenzelm@23704
   358
local
wenzelm@23704
   359
  val default = {output = default_output};
wenzelm@32738
   360
  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
wenzelm@23704
   361
in
wenzelm@23922
   362
  fun add_mode name output = CRITICAL (fn () =>
wenzelm@32738
   363
    Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
wenzelm@23704
   364
  fun get_mode () =
wenzelm@24612
   365
    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
wenzelm@23623
   366
end;
wenzelm@23704
   367
wenzelm@38474
   368
fun output m = if is_empty m then no_output else #output (get_mode ()) m;
wenzelm@23704
   369
wenzelm@23719
   370
val enclose = output #-> Library.enclose;
wenzelm@23719
   371
wenzelm@25552
   372
fun markup m =
wenzelm@25552
   373
  let val (bg, en) = output m
wenzelm@25552
   374
  in Library.enclose (Output.escape bg) (Output.escape en) end;
wenzelm@25552
   375
wenzelm@23704
   376
end;