src/Pure/PIDE/markup.ML
author wenzelm
Tue Mar 13 11:21:26 2012 +0100 (2012-03-13 ago)
changeset 46894 e2ad717ec889
parent 45674 eb65c9d17e2f
child 50201 c26369c9eda6
permissions -rw-r--r--
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm@45670
     1
(*  Title:      Pure/PIDE/markup.ML
wenzelm@23623
     2
    Author:     Makarius
wenzelm@23623
     3
wenzelm@45666
     4
Generic 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@40131
    18
  val no_output: Output.output * Output.output
wenzelm@40131
    19
  val default_output: T -> Output.output * Output.output
wenzelm@40131
    20
  val add_mode: string -> (T -> Output.output * Output.output) -> unit
wenzelm@40131
    21
  val output: T -> Output.output * Output.output
wenzelm@40131
    22
  val enclose: T -> Output.output -> Output.output
wenzelm@25552
    23
  val markup: T -> string -> string
wenzelm@43665
    24
  val markup_only: T -> string
wenzelm@23623
    25
end;
wenzelm@23623
    26
wenzelm@23623
    27
structure Markup: MARKUP =
wenzelm@23623
    28
struct
wenzelm@23623
    29
wenzelm@30221
    30
(** markup elements **)
wenzelm@30221
    31
wenzelm@38414
    32
(* integers *)
wenzelm@38414
    33
wenzelm@38414
    34
fun parse_int s =
wenzelm@43797
    35
  let val i = Int.fromString s in
wenzelm@43797
    36
    if is_none i orelse String.isPrefix "~" s
wenzelm@43797
    37
    then raise Fail ("Bad integer: " ^ quote s)
wenzelm@43797
    38
    else the i
wenzelm@43797
    39
  end;
wenzelm@38414
    40
wenzelm@38414
    41
val print_int = signed_string_of_int;
wenzelm@38414
    42
wenzelm@38414
    43
wenzelm@23658
    44
(* basic markup *)
wenzelm@23623
    45
wenzelm@28017
    46
type T = string * Properties.T;
wenzelm@23637
    47
wenzelm@38474
    48
val empty = ("", []);
wenzelm@23637
    49
wenzelm@38474
    50
fun is_empty ("", _) = true
wenzelm@38474
    51
  | is_empty _ = false;
wenzelm@27883
    52
wenzelm@23794
    53
wenzelm@23671
    54
fun properties more_props ((elem, props): T) =
wenzelm@28017
    55
  (elem, fold_rev Properties.put more_props props);
wenzelm@23671
    56
wenzelm@26977
    57
wenzelm@38721
    58
(* misc properties *)
wenzelm@26977
    59
wenzelm@23658
    60
val nameN = "name";
wenzelm@27818
    61
fun name a = properties [(nameN, a)];
wenzelm@27818
    62
wenzelm@23658
    63
val kindN = "kind";
wenzelm@23671
    64
wenzelm@23658
    65
wenzelm@27969
    66
wenzelm@30221
    67
(** print mode operations **)
wenzelm@23704
    68
wenzelm@29325
    69
val no_output = ("", "");
wenzelm@29325
    70
fun default_output (_: T) = no_output;
wenzelm@23704
    71
wenzelm@23704
    72
local
wenzelm@23704
    73
  val default = {output = default_output};
wenzelm@43684
    74
  val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
wenzelm@23704
    75
in
wenzelm@43684
    76
  fun add_mode name output =
wenzelm@46894
    77
    Synchronized.change modes (fn tab =>
wenzelm@46894
    78
      (if not (Symtab.defined tab name) then ()
wenzelm@46894
    79
       else warning ("Redefining markup mode " ^ quote name);
wenzelm@46894
    80
       Symtab.update (name, {output = output}) tab));
wenzelm@23704
    81
  fun get_mode () =
wenzelm@43684
    82
    the_default default
wenzelm@43684
    83
      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
wenzelm@23623
    84
end;
wenzelm@23704
    85
wenzelm@38474
    86
fun output m = if is_empty m then no_output else #output (get_mode ()) m;
wenzelm@23704
    87
wenzelm@23719
    88
val enclose = output #-> Library.enclose;
wenzelm@23719
    89
wenzelm@25552
    90
fun markup m =
wenzelm@25552
    91
  let val (bg, en) = output m
wenzelm@25552
    92
  in Library.enclose (Output.escape bg) (Output.escape en) end;
wenzelm@25552
    93
wenzelm@43665
    94
fun markup_only m = markup m "";
wenzelm@43665
    95
wenzelm@23704
    96
end;