src/Pure/PIDE/markup.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 46894 e2ad717ec889
child 50201 c26369c9eda6
permissions -rw-r--r--
more official command specifications, including source position;
     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 (fn tab =>
    78       (if not (Symtab.defined tab name) then ()
    79        else warning ("Redefining markup mode " ^ quote name);
    80        Symtab.update (name, {output = output}) tab));
    81   fun get_mode () =
    82     the_default default
    83       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
    84 end;
    85 
    86 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
    87 
    88 val enclose = output #-> Library.enclose;
    89 
    90 fun markup m =
    91   let val (bg, en) = output m
    92   in Library.enclose (Output.escape bg) (Output.escape en) end;
    93 
    94 fun markup_only m = markup m "";
    95 
    96 end;