src/Pure/General/markup.ML
author wenzelm
Sun, 25 Oct 2009 20:54:21 +0100
changeset 33172 61ee96bc9895
parent 33167 f02b804305d6
child 33643 b275f26a638b
permissions -rw-r--r--
maintain theory name via name space, not tags; AxClass.thynames_of_arity: explicit theory name, not tags;
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
    Author:     Makarius
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     3
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     4
Common markup elements.
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     5
*)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     6
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     7
signature MARKUP =
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     8
sig
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27969
diff changeset
     9
  type T = string * Properties.T
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    10
  val none: T
27883
e506f0c6d3f0 added is_none;
wenzelm
parents: 27879
diff changeset
    11
  val is_none: T -> bool
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    12
  val properties: (string * string) list -> T -> T
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    13
  val nameN: string
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
    14
  val name: string -> T -> T
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
    15
  val bindingN: string val binding: string -> T
23658
wenzelm
parents: 23644
diff changeset
    16
  val kindN: string
24777
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
    17
  val internalK: string
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
    18
  val entityN: string val entity: string -> T
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
    19
  val defN: string
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
    20
  val refN: string
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    21
  val lineN: string
26001
d0a133941155 added column property;
wenzelm
parents: 25982
diff changeset
    22
  val columnN: string
27794
bdea6e17cbe3 added offset/end_offset;
wenzelm
parents: 27748
diff changeset
    23
  val offsetN: string
27735
044901e02cc6 added end_line, end_column properties;
wenzelm
parents: 27660
diff changeset
    24
  val end_lineN: string
044901e02cc6 added end_line, end_column properties;
wenzelm
parents: 27660
diff changeset
    25
  val end_columnN: string
27794
bdea6e17cbe3 added offset/end_offset;
wenzelm
parents: 27748
diff changeset
    26
  val end_offsetN: string
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    27
  val fileN: string
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
    28
  val idN: string
27748
c421ee0d2350 added position_properties';
wenzelm
parents: 27743
diff changeset
    29
  val position_properties': string list
26051
43bcb30a6d97 added position_properties;
wenzelm
parents: 26001
diff changeset
    30
  val position_properties: string list
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    31
  val positionN: string val position: T
26255
2246d8bbe89d added location;
wenzelm
parents: 26051
diff changeset
    32
  val locationN: string val location: T
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
    33
  val indentN: string
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    34
  val blockN: string val block: int -> T
23695
6c4662bb4862 Add widthN to signature
aspinall
parents: 23671
diff changeset
    35
  val widthN: string
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
    36
  val breakN: string val break: int -> T
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
    37
  val fbreakN: string val fbreak: T
27828
edafacb690a3 renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
wenzelm
parents: 27818
diff changeset
    38
  val tclassN: string val tclass: string -> T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    39
  val tyconN: string val tycon: string -> T
28077
d6102a4fcfce added fixed_decl, fact_decl, local_fact_decl;
wenzelm
parents: 28031
diff changeset
    40
  val fixed_declN: string val fixed_decl: string -> T
26702
a079f8f0080b added markup for fixed variables (local constants);
wenzelm
parents: 26255
diff changeset
    41
  val fixedN: string val fixed: string -> T
28113
f6e38928b77c added const_decl;
wenzelm
parents: 28077
diff changeset
    42
  val const_declN: string val const_decl: string -> T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    43
  val constN: string val const: string -> T
28077
d6102a4fcfce added fixed_decl, fact_decl, local_fact_decl;
wenzelm
parents: 28031
diff changeset
    44
  val fact_declN: string val fact_decl: string -> T
27740
0b22524c05e2 removed axiom;
wenzelm
parents: 27735
diff changeset
    45
  val factN: string val fact: string -> T
0b22524c05e2 removed axiom;
wenzelm
parents: 27735
diff changeset
    46
  val dynamic_factN: string val dynamic_fact: string -> T
28077
d6102a4fcfce added fixed_decl, fact_decl, local_fact_decl;
wenzelm
parents: 28031
diff changeset
    47
  val local_fact_declN: string val local_fact_decl: string -> T
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
    48
  val local_factN: string val local_fact: string -> T
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    49
  val tfreeN: string val tfree: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    50
  val tvarN: string val tvar: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    51
  val freeN: string val free: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    52
  val skolemN: string val skolem: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    53
  val boundN: string val bound: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    54
  val varN: string val var: T
29318
6337d1cb2ba0 added numeral, which supercedes num, xnum, float;
wenzelm
parents: 28904
diff changeset
    55
  val numeralN: string val numeral: T
27804
f682666352c4 added literal;
wenzelm
parents: 27794
diff changeset
    56
  val literalN: string val literal: T
29318
6337d1cb2ba0 added numeral, which supercedes num, xnum, float;
wenzelm
parents: 28904
diff changeset
    57
  val inner_stringN: string val inner_string: T
27883
e506f0c6d3f0 added is_none;
wenzelm
parents: 27879
diff changeset
    58
  val inner_commentN: string val inner_comment: T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    59
  val sortN: string val sort: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    60
  val typN: string val typ: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    61
  val termN: string val term: T
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
    62
  val propN: string val prop: T
27748
c421ee0d2350 added position_properties';
wenzelm
parents: 27743
diff changeset
    63
  val attributeN: string val attribute: string -> T
c421ee0d2350 added position_properties';
wenzelm
parents: 27743
diff changeset
    64
  val methodN: string val method: string -> T
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
    65
  val ML_keywordN: string val ML_keyword: T
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
    66
  val ML_identN: string val ML_ident: T
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
    67
  val ML_tvarN: string val ML_tvar: T
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
    68
  val ML_numeralN: string val ML_numeral: T
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
    69
  val ML_charN: string val ML_char: T
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
    70
  val ML_stringN: string val ML_string: T
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
    71
  val ML_commentN: string val ML_comment: T
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
    72
  val ML_malformedN: string val ML_malformed: T
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30614
diff changeset
    73
  val ML_defN: string val ML_def: T
31472
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
    74
  val ML_openN: string val ML_open: T
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
    75
  val ML_structN: string val ML_struct: T
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30614
diff changeset
    76
  val ML_refN: string val ML_ref: T
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30614
diff changeset
    77
  val ML_typingN: string val ML_typing: T
27875
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
    78
  val ML_sourceN: string val ML_source: T
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
    79
  val doc_sourceN: string val doc_source: T
27879
wenzelm
parents: 27875
diff changeset
    80
  val antiqN: string val antiq: T
27894
a06f78f917e0 added ML_antiq, doc_antiq;
wenzelm
parents: 27883
diff changeset
    81
  val ML_antiqN: string val ML_antiq: string -> T
a06f78f917e0 added ML_antiq, doc_antiq;
wenzelm
parents: 27883
diff changeset
    82
  val doc_antiqN: string val doc_antiq: string -> T
27836
74e8228757c5 renamed unknown_span to malformed_span;
wenzelm
parents: 27828
diff changeset
    83
  val keyword_declN: string val keyword_decl: string -> T
74e8228757c5 renamed unknown_span to malformed_span;
wenzelm
parents: 27828
diff changeset
    84
  val command_declN: string val command_decl: string -> string -> T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    85
  val keywordN: string val keyword: string -> T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    86
  val commandN: string val command: string -> T
27836
74e8228757c5 renamed unknown_span to malformed_span;
wenzelm
parents: 27828
diff changeset
    87
  val identN: string val ident: T
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    88
  val stringN: string val string: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    89
  val altstringN: string val altstring: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    90
  val verbatimN: string val verbatim: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    91
  val commentN: string val comment: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    92
  val controlN: string val control: T
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    93
  val malformedN: string val malformed: T
27851
wenzelm
parents: 27836
diff changeset
    94
  val tokenN: string val token: T
27660
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
    95
  val command_spanN: string val command_span: string -> T
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
    96
  val ignored_spanN: string val ignored_span: T
27836
74e8228757c5 renamed unknown_span to malformed_span;
wenzelm
parents: 27828
diff changeset
    97
  val malformed_spanN: string val malformed_span: T
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    98
  val stateN: string val state: T
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    99
  val subgoalN: string val subgoal: T
24289
bfd59eb6e24e added sendback;
wenzelm
parents: 23922
diff changeset
   100
  val sendbackN: string val sendback: T
24555
ea220faa69e7 added hilite markup;
wenzelm
parents: 24289
diff changeset
   101
  val hiliteN: string val hilite: T
29417
779ff1187327 added running task markup;
wenzelm
parents: 29325
diff changeset
   102
  val taskN: string
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   103
  val unprocessedN: string val unprocessed: T
29417
779ff1187327 added running task markup;
wenzelm
parents: 29325
diff changeset
   104
  val runningN: string val running: string -> T
27615
wenzelm
parents: 27606
diff changeset
   105
  val failedN: string val failed: T
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   106
  val finishedN: string val finished: T
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   107
  val disposedN: string val disposed: T
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   108
  val editsN: string val edits: string -> T
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   109
  val editN: string val edit: string -> string -> T
27969
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   110
  val pidN: string
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   111
  val sessionN: string
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   112
  val promptN: string val prompt: T
31384
ce169bd37fc0 IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents: 30702
diff changeset
   113
  val readyN: string val ready: T
29325
a205acc94356 Markup.no_output;
wenzelm
parents: 29318
diff changeset
   114
  val no_output: output * output
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   115
  val default_output: T -> output * output
23786
3390bb8cf681 removed ident, space;
wenzelm
parents: 23719
diff changeset
   116
  val add_mode: string -> (T -> output * output) -> unit
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   117
  val output: T -> output * output
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   118
  val enclose: T -> output -> output
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   119
  val markup: T -> string -> string
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   120
end;
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   121
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   122
structure Markup: MARKUP =
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   123
struct
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   124
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
   125
(** markup elements **)
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
   126
23658
wenzelm
parents: 23644
diff changeset
   127
(* basic markup *)
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   128
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27969
diff changeset
   129
type T = string * Properties.T;
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   130
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   131
val none = ("", []);
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   132
27883
e506f0c6d3f0 added is_none;
wenzelm
parents: 27879
diff changeset
   133
fun is_none ("", _) = true
e506f0c6d3f0 added is_none;
wenzelm
parents: 27879
diff changeset
   134
  | is_none _ = false;
e506f0c6d3f0 added is_none;
wenzelm
parents: 27879
diff changeset
   135
23794
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
   136
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   137
fun properties more_props ((elem, props): T) =
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27969
diff changeset
   138
  (elem, fold_rev Properties.put more_props props);
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   139
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   140
fun markup_elem elem = (elem, (elem, []): T);
23794
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
   141
fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
   142
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
   143
26977
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
   144
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
   145
(* name *)
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
   146
23658
wenzelm
parents: 23644
diff changeset
   147
val nameN = "name";
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
   148
fun name a = properties [(nameN, a)];
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
   149
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
   150
val (bindingN, binding) = markup_string "binding" nameN;
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
   151
24777
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   152
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   153
(* kind *)
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   154
23658
wenzelm
parents: 23644
diff changeset
   155
val kindN = "kind";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   156
24777
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   157
val internalK = "internal";
c1250851d701 added internalK, property_internal;
wenzelm
parents: 24612
diff changeset
   158
23658
wenzelm
parents: 23644
diff changeset
   159
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   160
(* formal entities *)
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   161
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   162
val (entityN, entity) = markup_string "entity" nameN;
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   163
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   164
val defN = "def";
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   165
val refN = "ref";
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   166
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32738
diff changeset
   167
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   168
(* position *)
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   169
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   170
val lineN = "line";
26001
d0a133941155 added column property;
wenzelm
parents: 25982
diff changeset
   171
val columnN = "column";
27794
bdea6e17cbe3 added offset/end_offset;
wenzelm
parents: 27748
diff changeset
   172
val offsetN = "offset";
27735
044901e02cc6 added end_line, end_column properties;
wenzelm
parents: 27660
diff changeset
   173
val end_lineN = "end_line";
044901e02cc6 added end_line, end_column properties;
wenzelm
parents: 27660
diff changeset
   174
val end_columnN = "end_column";
27794
bdea6e17cbe3 added offset/end_offset;
wenzelm
parents: 27748
diff changeset
   175
val end_offsetN = "end_offset";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   176
val fileN = "file";
25816
d2a94e6a7d1e moved id to position properties;
wenzelm
parents: 25808
diff changeset
   177
val idN = "id";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
   178
27794
bdea6e17cbe3 added offset/end_offset;
wenzelm
parents: 27748
diff changeset
   179
val position_properties' = [end_lineN, end_columnN, end_offsetN, fileN, idN];
bdea6e17cbe3 added offset/end_offset;
wenzelm
parents: 27748
diff changeset
   180
val position_properties = [lineN, columnN, offsetN] @ position_properties';
27748
c421ee0d2350 added position_properties';
wenzelm
parents: 27743
diff changeset
   181
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   182
val (positionN, position) = markup_elem "position";
26255
2246d8bbe89d added location;
wenzelm
parents: 26051
diff changeset
   183
val (locationN, location) = markup_elem "location";
2246d8bbe89d added location;
wenzelm
parents: 26051
diff changeset
   184
23644
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   185
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   186
(* pretty printing *)
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   187
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   188
val indentN = "indent";
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   189
val (blockN, block) = markup_int "block" indentN;
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   190
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   191
val widthN = "width";
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   192
val (breakN, break) = markup_int "break" widthN;
e28b8e8a85b6 added markup for pretty printing;
wenzelm
parents: 23642
diff changeset
   193
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   194
val (fbreakN, fbreak) = markup_elem "fbreak";
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   195
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   196
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   197
(* logical entities *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   198
27828
edafacb690a3 renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
wenzelm
parents: 27818
diff changeset
   199
val (tclassN, tclass) = markup_string "tclass" nameN;
23658
wenzelm
parents: 23644
diff changeset
   200
val (tyconN, tycon) = markup_string "tycon" nameN;
28077
d6102a4fcfce added fixed_decl, fact_decl, local_fact_decl;
wenzelm
parents: 28031
diff changeset
   201
val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN;
26702
a079f8f0080b added markup for fixed variables (local constants);
wenzelm
parents: 26255
diff changeset
   202
val (fixedN, fixed) = markup_string "fixed" nameN;
28113
f6e38928b77c added const_decl;
wenzelm
parents: 28077
diff changeset
   203
val (const_declN, const_decl) = markup_string "const_decl" nameN;
23658
wenzelm
parents: 23644
diff changeset
   204
val (constN, const) = markup_string "const" nameN;
28077
d6102a4fcfce added fixed_decl, fact_decl, local_fact_decl;
wenzelm
parents: 28031
diff changeset
   205
val (fact_declN, fact_decl) = markup_string "fact_decl" nameN;
27740
0b22524c05e2 removed axiom;
wenzelm
parents: 27735
diff changeset
   206
val (factN, fact) = markup_string "fact" nameN;
0b22524c05e2 removed axiom;
wenzelm
parents: 27735
diff changeset
   207
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
28077
d6102a4fcfce added fixed_decl, fact_decl, local_fact_decl;
wenzelm
parents: 28031
diff changeset
   208
val (local_fact_declN, local_fact_decl) = markup_string "local_fact_decl" nameN;
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
   209
val (local_factN, local_fact) = markup_string "local_fact" nameN;
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   210
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   211
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   212
(* inner syntax *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   213
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   214
val (tfreeN, tfree) = markup_elem "tfree";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   215
val (tvarN, tvar) = markup_elem "tvar";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   216
val (freeN, free) = markup_elem "free";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   217
val (skolemN, skolem) = markup_elem "skolem";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   218
val (boundN, bound) = markup_elem "bound";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   219
val (varN, var) = markup_elem "var";
29318
6337d1cb2ba0 added numeral, which supercedes num, xnum, float;
wenzelm
parents: 28904
diff changeset
   220
val (numeralN, numeral) = markup_elem "numeral";
27804
f682666352c4 added literal;
wenzelm
parents: 27794
diff changeset
   221
val (literalN, literal) = markup_elem "literal";
29318
6337d1cb2ba0 added numeral, which supercedes num, xnum, float;
wenzelm
parents: 28904
diff changeset
   222
val (inner_stringN, inner_string) = markup_elem "inner_string";
27883
e506f0c6d3f0 added is_none;
wenzelm
parents: 27879
diff changeset
   223
val (inner_commentN, inner_comment) = markup_elem "inner_comment";
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   224
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   225
val (sortN, sort) = markup_elem "sort";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   226
val (typN, typ) = markup_elem "typ";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   227
val (termN, term) = markup_elem "term";
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
   228
val (propN, prop) = markup_elem "prop";
27748
c421ee0d2350 added position_properties';
wenzelm
parents: 27743
diff changeset
   229
c421ee0d2350 added position_properties';
wenzelm
parents: 27743
diff changeset
   230
val (attributeN, attribute) = markup_string "attribute" nameN;
c421ee0d2350 added position_properties';
wenzelm
parents: 27743
diff changeset
   231
val (methodN, method) = markup_string "method" nameN;
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   232
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   233
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   234
(* ML syntax *)
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   235
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   236
val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   237
val (ML_identN, ML_ident) = markup_elem "ML_ident";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   238
val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   239
val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   240
val (ML_charN, ML_char) = markup_elem "ML_char";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   241
val (ML_stringN, ML_string) = markup_elem "ML_string";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   242
val (ML_commentN, ML_comment) = markup_elem "ML_comment";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   243
val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   244
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30614
diff changeset
   245
val (ML_defN, ML_def) = markup_elem "ML_def";
31472
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   246
val (ML_openN, ML_open) = markup_elem "ML_open";
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   247
val (ML_structN, ML_struct) = markup_elem "ML_struct";
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30614
diff changeset
   248
val (ML_refN, ML_ref) = markup_elem "ML_ref";
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30614
diff changeset
   249
val (ML_typingN, ML_typing) = markup_elem "ML_typing";
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30614
diff changeset
   250
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30221
diff changeset
   251
27875
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   252
(* embedded source text *)
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   253
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   254
val (ML_sourceN, ML_source) = markup_elem "ML_source";
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   255
val (doc_sourceN, doc_source) = markup_elem "doc_source";
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   256
27879
wenzelm
parents: 27875
diff changeset
   257
val (antiqN, antiq) = markup_elem "antiq";
27894
a06f78f917e0 added ML_antiq, doc_antiq;
wenzelm
parents: 27883
diff changeset
   258
val (ML_antiqN, ML_antiq) = markup_string "ML_antiq" nameN;
a06f78f917e0 added ML_antiq, doc_antiq;
wenzelm
parents: 27883
diff changeset
   259
val (doc_antiqN, doc_antiq) = markup_string "doc_antiq" nameN;
27879
wenzelm
parents: 27875
diff changeset
   260
27875
1b46d9ec3788 added ML_source, doc_source;
wenzelm
parents: 27851
diff changeset
   261
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   262
(* outer syntax *)
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   263
24870
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   264
val (keyword_declN, keyword_decl) = markup_string "keyword_decl" nameN;
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   265
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   266
val command_declN = "command_decl";
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   267
fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
9d057ff8e74c added keyword_decl, command_decl;
wenzelm
parents: 24777
diff changeset
   268
27836
74e8228757c5 renamed unknown_span to malformed_span;
wenzelm
parents: 27828
diff changeset
   269
val (keywordN, keyword) = markup_string "keyword" nameN;
74e8228757c5 renamed unknown_span to malformed_span;
wenzelm
parents: 27828
diff changeset
   270
val (commandN, command) = markup_string "command" nameN;
74e8228757c5 renamed unknown_span to malformed_span;
wenzelm
parents: 27828
diff changeset
   271
val (identN, ident) = markup_elem "ident";
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   272
val (stringN, string) = markup_elem "string";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   273
val (altstringN, altstring) = markup_elem "altstring";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   274
val (verbatimN, verbatim) = markup_elem "verbatim";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   275
val (commentN, comment) = markup_elem "comment";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   276
val (controlN, control) = markup_elem "control";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   277
val (malformedN, malformed) = markup_elem "malformed";
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   278
27851
wenzelm
parents: 27836
diff changeset
   279
val (tokenN, token) = markup_elem "token";
wenzelm
parents: 27836
diff changeset
   280
27660
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
   281
val (command_spanN, command_span) = markup_string "command_span" nameN;
61fef1137a25 renamed command span markup;
wenzelm
parents: 27615
diff changeset
   282
val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
27836
74e8228757c5 renamed unknown_span to malformed_span;
wenzelm
parents: 27828
diff changeset
   283
val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   284
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   285
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   286
(* toplevel *)
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
   287
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   288
val (stateN, state) = markup_elem "state";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   289
val (subgoalN, subgoal) = markup_elem "subgoal";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   290
val (sendbackN, sendback) = markup_elem "sendback";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   291
val (hiliteN, hilite) = markup_elem "hilite";
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   292
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   293
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   294
(* command status *)
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   295
29417
779ff1187327 added running task markup;
wenzelm
parents: 29325
diff changeset
   296
val taskN = "task";
779ff1187327 added running task markup;
wenzelm
parents: 29325
diff changeset
   297
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   298
val (unprocessedN, unprocessed) = markup_elem "unprocessed";
29417
779ff1187327 added running task markup;
wenzelm
parents: 29325
diff changeset
   299
val (runningN, running) = markup_string "running" taskN;
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
val (disposedN, disposed) = markup_elem "disposed";
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   303
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   304
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   305
(* interactive documents *)
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   306
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   307
val (editsN, edits) = markup_string "edits" idN;
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   308
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   309
val editN = "edit";
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   310
fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]);
29482
fe044b49e34f added command_state markup;
wenzelm
parents: 29417
diff changeset
   311
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27523
diff changeset
   312
27969
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   313
(* messages *)
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   314
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   315
val pidN = "pid";
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   316
val sessionN = "session";
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   317
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   318
val (promptN, prompt) = markup_elem "prompt";
31384
ce169bd37fc0 IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents: 30702
diff changeset
   319
val (readyN, ready) = markup_elem "ready";
27969
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   320
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   321
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
   322
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
   323
(** print mode operations **)
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   324
29325
a205acc94356 Markup.no_output;
wenzelm
parents: 29318
diff changeset
   325
val no_output = ("", "");
a205acc94356 Markup.no_output;
wenzelm
parents: 29318
diff changeset
   326
fun default_output (_: T) = no_output;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   327
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   328
local
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   329
  val default = {output = default_output};
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31472
diff changeset
   330
  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   331
in
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23794
diff changeset
   332
  fun add_mode name output = CRITICAL (fn () =>
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31472
diff changeset
   333
    Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   334
  fun get_mode () =
24612
d1b315bdb8d7 avoid direct access to print_mode;
wenzelm
parents: 24555
diff changeset
   335
    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
   336
end;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   337
29325
a205acc94356 Markup.no_output;
wenzelm
parents: 29318
diff changeset
   338
fun output m = if is_none m then no_output else #output (get_mode ()) m;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   339
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   340
val enclose = output #-> Library.enclose;
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
   341
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   342
fun markup m =
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   343
  let val (bg, en) = output m
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   344
  in Library.enclose (Output.escape bg) (Output.escape en) end;
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
   345
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
   346
end;