src/Pure/PIDE/markup.ML
author wenzelm
Tue Nov 29 21:50:00 2011 +0100 (2011-11-29 ago)
changeset 45674 eb65c9d17e2f
parent 45670 b84170538043
child 46894 e2ad717ec889
permissions -rw-r--r--
clarified Time vs. Timing;
     1 (*  Title:      Pure/PIDE/markup.ML
     2     Author:     Makarius
     3 
     4 Generic markup elements.
     5 *)
     6 
     7 signature MARKUP =
     8 sig
     9   val parse_int: string -> int
    10   val print_int: int -> string
    11   type T = string * Properties.T
    12   val empty: T
    13   val is_empty: T -> bool
    14   val properties: Properties.T -> T -> T
    15   val nameN: string
    16   val name: string -> T -> T
    17   val kindN: string
    18   val no_output: Output.output * Output.output
    19   val default_output: T -> Output.output * Output.output
    20   val add_mode: string -> (T -> Output.output * Output.output) -> unit
    21   val output: T -> Output.output * Output.output
    22   val enclose: T -> Output.output -> Output.output
    23   val markup: T -> string -> string
    24   val markup_only: T -> string
    25 end;
    26 
    27 structure Markup: MARKUP =
    28 struct
    29 
    30 (** markup elements **)
    31 
    32 (* integers *)
    33 
    34 fun parse_int s =
    35   let val i = Int.fromString s in
    36     if is_none i orelse String.isPrefix "~" s
    37     then raise Fail ("Bad integer: " ^ quote s)
    38     else the i
    39   end;
    40 
    41 val print_int = signed_string_of_int;
    42 
    43 
    44 (* basic markup *)
    45 
    46 type T = string * Properties.T;
    47 
    48 val empty = ("", []);
    49 
    50 fun is_empty ("", _) = true
    51   | is_empty _ = false;
    52 
    53 
    54 fun properties more_props ((elem, props): T) =
    55   (elem, fold_rev Properties.put more_props props);
    56 
    57 
    58 (* misc properties *)
    59 
    60 val nameN = "name";
    61 fun name a = properties [(nameN, a)];
    62 
    63 val kindN = "kind";
    64 
    65 
    66 
    67 (** print mode operations **)
    68 
    69 val no_output = ("", "");
    70 fun default_output (_: T) = no_output;
    71 
    72 local
    73   val default = {output = default_output};
    74   val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
    75 in
    76   fun add_mode name output =
    77     Synchronized.change modes (Symtab.update_new (name, {output = output}));
    78   fun get_mode () =
    79     the_default default
    80       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
    81 end;
    82 
    83 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
    84 
    85 val enclose = output #-> Library.enclose;
    86 
    87 fun markup m =
    88   let val (bg, en) = output m
    89   in Library.enclose (Output.escape bg) (Output.escape en) end;
    90 
    91 fun markup_only m = markup m "";
    92 
    93 end;