src/Pure/PIDE/markup.ML
author wenzelm
Tue, 29 Nov 2011 21:50:00 +0100
changeset 45674 eb65c9d17e2f
parent 45670 b84170538043
child 46894 e2ad717ec889
permissions -rw-r--r--
clarified Time vs. Timing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45670
b84170538043 rearranged files;
wenzelm
parents: 45666
diff changeset
     1
(*  Title:      Pure/PIDE/markup.ML
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
     3
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45445
diff changeset
     4
Generic markup elements.
23623
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
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
     9
  val parse_int: string -> int
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
    10
  val print_int: int -> string
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27969
diff changeset
    11
  type T = string * Properties.T
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    12
  val empty: T
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    13
  val is_empty: T -> bool
38229
61d0fe8b96ac more robust treatment of Markup.token;
wenzelm
parents: 37195
diff changeset
    14
  val properties: Properties.T -> T -> T
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    15
  val nameN: string
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
    16
  val name: string -> T -> T
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38871
diff changeset
    17
  val kindN: string
40131
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 39585
diff changeset
    18
  val no_output: Output.output * Output.output
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 39585
diff changeset
    19
  val default_output: T -> Output.output * Output.output
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 39585
diff changeset
    20
  val add_mode: string -> (T -> Output.output * Output.output) -> unit
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 39585
diff changeset
    21
  val output: T -> Output.output * Output.output
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 39585
diff changeset
    22
  val enclose: T -> Output.output -> Output.output
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
    23
  val markup: T -> string -> string
43665
573d1272f36d tuned signature;
wenzelm
parents: 43593
diff changeset
    24
  val markup_only: T -> string
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    25
end;
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    26
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    27
structure Markup: MARKUP =
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    28
struct
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    29
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
    30
(** markup elements **)
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
    31
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
    32
(* integers *)
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
    33
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
    34
fun parse_int s =
43797
fad7758421bf more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents: 43748
diff changeset
    35
  let val i = Int.fromString s in
fad7758421bf more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents: 43748
diff changeset
    36
    if is_none i orelse String.isPrefix "~" s
fad7758421bf more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents: 43748
diff changeset
    37
    then raise Fail ("Bad integer: " ^ quote s)
fad7758421bf more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents: 43748
diff changeset
    38
    else the i
fad7758421bf more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
wenzelm
parents: 43748
diff changeset
    39
  end;
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
    40
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
    41
val print_int = signed_string_of_int;
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
    42
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38229
diff changeset
    43
23658
wenzelm
parents: 23644
diff changeset
    44
(* basic markup *)
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    45
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27969
diff changeset
    46
type T = string * Properties.T;
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    47
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    48
val empty = ("", []);
23637
f3e16ee56f32 added toplevel markup;
wenzelm
parents: 23626
diff changeset
    49
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    50
fun is_empty ("", _) = true
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    51
  | is_empty _ = false;
27883
e506f0c6d3f0 added is_none;
wenzelm
parents: 27879
diff changeset
    52
23794
ab2edd87b912 added get_string, get_int;
wenzelm
parents: 23786
diff changeset
    53
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    54
fun properties more_props ((elem, props): T) =
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27969
diff changeset
    55
  (elem, fold_rev Properties.put more_props props);
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    56
26977
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
    57
38721
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
    58
(* misc properties *)
26977
e736139b553d added theory_nameN;
wenzelm
parents: 26702
diff changeset
    59
23658
wenzelm
parents: 23644
diff changeset
    60
val nameN = "name";
27818
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
    61
fun name a = properties [(nameN, a)];
74087a19879f added name property operation;
wenzelm
parents: 27804
diff changeset
    62
23658
wenzelm
parents: 23644
diff changeset
    63
val kindN = "kind";
23671
9e8257472c27 proper position markup;
wenzelm
parents: 23658
diff changeset
    64
23658
wenzelm
parents: 23644
diff changeset
    65
27969
46d7057b8614 added messages and process information;
wenzelm
parents: 27894
diff changeset
    66
30221
14145e81a2fe added markup for binding;
wenzelm
parents: 29522
diff changeset
    67
(** print mode operations **)
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    68
29325
a205acc94356 Markup.no_output;
wenzelm
parents: 29318
diff changeset
    69
val no_output = ("", "");
a205acc94356 Markup.no_output;
wenzelm
parents: 29318
diff changeset
    70
fun default_output (_: T) = no_output;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    71
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    72
local
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    73
  val default = {output = default_output};
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    74
  val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    75
in
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    76
  fun add_mode name output =
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    77
    Synchronized.change modes (Symtab.update_new (name, {output = output}));
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    78
  fun get_mode () =
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    79
    the_default default
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    80
      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
23623
939b58b527ee Common markup elements.
wenzelm
parents:
diff changeset
    81
end;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    82
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    83
fun output m = if is_empty m then no_output else #output (get_mode ()) m;
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    84
23719
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    85
val enclose = output #-> Library.enclose;
ccd9cb15c062 more markup for inner and outer syntax;
wenzelm
parents: 23704
diff changeset
    86
25552
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
    87
fun markup m =
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
    88
  let val (bg, en) = output m
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
    89
  in Library.enclose (Output.escape bg) (Output.escape en) end;
e4d465bc5b35 added channels;
wenzelm
parents: 24870
diff changeset
    90
43665
573d1272f36d tuned signature;
wenzelm
parents: 43593
diff changeset
    91
fun markup_only m = markup m "";
573d1272f36d tuned signature;
wenzelm
parents: 43593
diff changeset
    92
23704
18d6ee425689 added print_mode setup (from pretty.ML);
wenzelm
parents: 23695
diff changeset
    93
end;