src/Pure/General/markup.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23794 ab2edd87b912
child 23922 707639e9497d
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/General/markup.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Common markup elements.
     6 *)
     7 
     8 signature MARKUP =
     9 sig
    10   type property = string * string
    11   type T = string * property list
    12   val get_string: T -> string -> string option
    13   val get_int: T -> string -> int option
    14   val none: T
    15   val properties: (string * string) list -> T -> T
    16   val nameN: string
    17   val kindN: string
    18   val lineN: string
    19   val fileN: string
    20   val positionN: string val position: T
    21   val indentN: string
    22   val blockN: string val block: int -> T
    23   val widthN: string
    24   val breakN: string val break: int -> T
    25   val fbreakN: string val fbreak: T
    26   val classN: string val class: string -> T
    27   val tyconN: string val tycon: string -> T
    28   val constN: string val const: string -> T
    29   val axiomN: string val axiom: string -> T
    30   val tfreeN: string val tfree: T
    31   val tvarN: string val tvar: T
    32   val freeN: string val free: T
    33   val skolemN: string val skolem: T
    34   val boundN: string val bound: T
    35   val varN: string val var: T
    36   val numN: string val num: T
    37   val xnumN: string val xnum: T
    38   val xstrN: string val xstr: T
    39   val sortN: string val sort: T
    40   val typN: string val typ: T
    41   val termN: string val term: T
    42   val keywordN: string val keyword: string -> T
    43   val commandN: string val command: string -> T
    44   val stringN: string val string: T
    45   val altstringN: string val altstring: T
    46   val verbatimN: string val verbatim: T
    47   val commentN: string val comment: T
    48   val controlN: string val control: T
    49   val malformedN: string val malformed: T
    50   val antiqN: string val antiq: T
    51   val whitespaceN: string val whitespace: T
    52   val junkN: string val junk: T
    53   val commandspanN: string val commandspan: string -> T
    54   val promptN: string val prompt: T
    55   val stateN: string val state: T
    56   val subgoalN: string val subgoal: T
    57   val default_output: T -> output * output
    58   val add_mode: string -> (T -> output * output) -> unit
    59   val output: T -> output * output
    60   val enclose: T -> output -> output
    61 end;
    62 
    63 structure Markup: MARKUP =
    64 struct
    65 
    66 (* basic markup *)
    67 
    68 type property = string * string;
    69 type T = string * property list;
    70 
    71 val none = ("", []);
    72 
    73 
    74 fun properties more_props ((elem, props): T) =
    75   (elem, fold_rev (AList.update (op =)) more_props props);
    76 
    77 fun get_string ((_, props): T) prop = AList.lookup (op =) props prop;
    78 fun get_int m prop = (case get_string m prop of NONE => NONE | SOME s => Int.fromString s);
    79 
    80 fun markup elem = (elem, (elem, []): T);
    81 fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
    82 fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
    83 
    84 val nameN = "name";
    85 val kindN = "kind";
    86 
    87 
    88 (* position *)
    89 
    90 val lineN = "line";
    91 val fileN = "file";
    92 
    93 val (positionN, position) = markup "position";
    94 
    95 
    96 (* pretty printing *)
    97 
    98 val indentN = "indent";
    99 val (blockN, block) = markup_int "block" indentN;
   100 
   101 val widthN = "width";
   102 val (breakN, break) = markup_int "break" widthN;
   103 
   104 val (fbreakN, fbreak) = markup "fbreak";
   105 
   106 
   107 (* logical entities *)
   108 
   109 val (classN, class) = markup_string "class" nameN;
   110 val (tyconN, tycon) = markup_string "tycon" nameN;
   111 val (constN, const) = markup_string "const" nameN;
   112 val (axiomN, axiom) = markup_string "axiom" nameN;
   113 
   114 
   115 (* inner syntax *)
   116 
   117 val (tfreeN, tfree) = markup "tfree";
   118 val (tvarN, tvar) = markup "tvar";
   119 val (freeN, free) = markup "free";
   120 val (skolemN, skolem) = markup "skolem";
   121 val (boundN, bound) = markup "bound";
   122 val (varN, var) = markup "var";
   123 val (numN, num) = markup "num";
   124 val (xnumN, xnum) = markup "xnum";
   125 val (xstrN, xstr) = markup "xstr";
   126 
   127 val (sortN, sort) = markup "sort";
   128 val (typN, typ) = markup "typ";
   129 val (termN, term) = markup "term";
   130 
   131 
   132 (* outer syntax *)
   133 
   134 val (keywordN, keyword) = markup_string "keyword" nameN;
   135 val (commandN, command) = markup_string "command" nameN;
   136 
   137 val (stringN, string) = markup "string";
   138 val (altstringN, altstring) = markup "altstring";
   139 val (verbatimN, verbatim) = markup "verbatim";
   140 val (commentN, comment) = markup "comment";
   141 val (controlN, control) = markup "control";
   142 val (malformedN, malformed) = markup "malformed";
   143 
   144 val (antiqN, antiq) = markup "antiq";
   145 
   146 val (whitespaceN, whitespace) = markup "whitespace";
   147 val (junkN, junk) = markup "junk";
   148 val (commandspanN, commandspan) = markup_string "commandspan" nameN;
   149 
   150 
   151 (* toplevel *)
   152 
   153 val (promptN, prompt) = markup "prompt";
   154 val (stateN, state) = markup "state";
   155 val (subgoalN, subgoal) = markup "subgoal";
   156 
   157 
   158 (* print mode operations *)
   159 
   160 fun default_output (_: T) = ("", "");
   161 
   162 local
   163   val default = {output = default_output};
   164   val modes = ref (Symtab.make [("", default)]);
   165 in
   166   fun add_mode name output =
   167     change modes (Symtab.update_new (name, {output = output}));
   168   fun get_mode () =
   169     the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
   170 end;
   171 
   172 fun output ("", _) = ("", "")
   173   | output m = #output (get_mode ()) m;
   174 
   175 val enclose = output #-> Library.enclose;
   176 
   177 end;