src/Pure/General/markup.ML
changeset 27883 e506f0c6d3f0
parent 27879 67d14d7c7143
child 27894 a06f78f917e0
equal deleted inserted replaced
27882:eaa9fef9f4c1 27883:e506f0c6d3f0
    10   type property = string * string
    10   type property = string * string
    11   type T = string * property list
    11   type T = string * property list
    12   val get_string: T -> string -> string option
    12   val get_string: T -> string -> string option
    13   val get_int: T -> string -> int option
    13   val get_int: T -> string -> int option
    14   val none: T
    14   val none: T
       
    15   val is_none: T -> bool
    15   val properties: (string * string) list -> T -> T
    16   val properties: (string * string) list -> T -> T
    16   val nameN: string
    17   val nameN: string
    17   val name: string -> T -> T
    18   val name: string -> T -> T
    18   val groupN: string
    19   val groupN: string
    19   val theory_nameN: string
    20   val theory_nameN: string
    52   val varN: string val var: T
    53   val varN: string val var: T
    53   val numN: string val num: T
    54   val numN: string val num: T
    54   val xnumN: string val xnum: T
    55   val xnumN: string val xnum: T
    55   val xstrN: string val xstr: T
    56   val xstrN: string val xstr: T
    56   val literalN: string val literal: T
    57   val literalN: string val literal: T
       
    58   val inner_commentN: string val inner_comment: T
    57   val sortN: string val sort: T
    59   val sortN: string val sort: T
    58   val typN: string val typ: T
    60   val typN: string val typ: T
    59   val termN: string val term: T
    61   val termN: string val term: T
    60   val propN: string val prop: T
    62   val propN: string val prop: T
    61   val attributeN: string val attribute: string -> T
    63   val attributeN: string val attribute: string -> T
   103 type property = string * string;
   105 type property = string * string;
   104 type T = string * property list;
   106 type T = string * property list;
   105 
   107 
   106 val none = ("", []);
   108 val none = ("", []);
   107 
   109 
       
   110 fun is_none ("", _) = true
       
   111   | is_none _ = false;
       
   112 
   108 
   113 
   109 fun properties more_props ((elem, props): T) =
   114 fun properties more_props ((elem, props): T) =
   110   (elem, fold_rev (AList.update (op =)) more_props props);
   115   (elem, fold_rev (AList.update (op =)) more_props props);
   111 
   116 
   112 fun get_string ((_, props): T) prop = AList.lookup (op =) props prop;
   117 fun get_string ((_, props): T) prop = AList.lookup (op =) props prop;
   185 val (varN, var) = markup_elem "var";
   190 val (varN, var) = markup_elem "var";
   186 val (numN, num) = markup_elem "num";
   191 val (numN, num) = markup_elem "num";
   187 val (xnumN, xnum) = markup_elem "xnum";
   192 val (xnumN, xnum) = markup_elem "xnum";
   188 val (xstrN, xstr) = markup_elem "xstr";
   193 val (xstrN, xstr) = markup_elem "xstr";
   189 val (literalN, literal) = markup_elem "literal";
   194 val (literalN, literal) = markup_elem "literal";
       
   195 val (inner_commentN, inner_comment) = markup_elem "inner_comment";
   190 
   196 
   191 val (sortN, sort) = markup_elem "sort";
   197 val (sortN, sort) = markup_elem "sort";
   192 val (typN, typ) = markup_elem "typ";
   198 val (typN, typ) = markup_elem "typ";
   193 val (termN, term) = markup_elem "term";
   199 val (termN, term) = markup_elem "term";
   194 val (propN, prop) = markup_elem "prop";
   200 val (propN, prop) = markup_elem "prop";
   259     change modes (Symtab.update_new (name, {output = output})));
   265     change modes (Symtab.update_new (name, {output = output})));
   260   fun get_mode () =
   266   fun get_mode () =
   261     the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
   267     the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
   262 end;
   268 end;
   263 
   269 
   264 fun output ("", _) = ("", "")
   270 fun output m = if is_none m then ("", "") else #output (get_mode ()) m;
   265   | output m = #output (get_mode ()) m;
       
   266 
   271 
   267 val enclose = output #-> Library.enclose;
   272 val enclose = output #-> Library.enclose;
   268 
   273 
   269 fun markup m =
   274 fun markup m =
   270   let val (bg, en) = output m
   275   let val (bg, en) = output m