# HG changeset patch # User wenzelm # Date 1196896892 -3600 # Node ID e4d465bc5b35d99f042c313eb0f3d87bc5c4169f # Parent 87d89b0f847a5dfd96fadfb688c4eac45324bbd4 added channels; added markup operation, which operates on plain strings instead of raw output; diff -r 87d89b0f847a -r e4d465bc5b35 src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Thu Dec 06 00:21:30 2007 +0100 +++ b/src/Pure/General/markup.ML Thu Dec 06 00:21:32 2007 +0100 @@ -60,10 +60,17 @@ val subgoalN: string val subgoal: T val sendbackN: string val sendback: T val hiliteN: string val hilite: T + val writelnN: string val writeln: T + val priorityN: string val priority: T + val tracingN: string val tracing: T + val warningN: string val warning: T + val errorN: string val error: T + val debugN: string val debug: T val default_output: T -> output * output val add_mode: string -> (T -> output * output) -> unit val output: T -> output * output val enclose: T -> output -> output + val markup: T -> string -> string end; structure Markup: MARKUP = @@ -83,7 +90,7 @@ fun get_string ((_, props): T) prop = AList.lookup (op =) props prop; fun get_int m prop = (case get_string m prop of NONE => NONE | SOME s => Int.fromString s); -fun markup elem = (elem, (elem, []): T); +fun markup_elem elem = (elem, (elem, []): T); fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T); fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T); @@ -103,7 +110,7 @@ val lineN = "line"; val fileN = "file"; -val (positionN, position) = markup "position"; +val (positionN, position) = markup_elem "position"; (* pretty printing *) @@ -114,7 +121,7 @@ val widthN = "width"; val (breakN, break) = markup_int "break" widthN; -val (fbreakN, fbreak) = markup "fbreak"; +val (fbreakN, fbreak) = markup_elem "fbreak"; (* logical entities *) @@ -127,19 +134,19 @@ (* inner syntax *) -val (tfreeN, tfree) = markup "tfree"; -val (tvarN, tvar) = markup "tvar"; -val (freeN, free) = markup "free"; -val (skolemN, skolem) = markup "skolem"; -val (boundN, bound) = markup "bound"; -val (varN, var) = markup "var"; -val (numN, num) = markup "num"; -val (xnumN, xnum) = markup "xnum"; -val (xstrN, xstr) = markup "xstr"; +val (tfreeN, tfree) = markup_elem "tfree"; +val (tvarN, tvar) = markup_elem "tvar"; +val (freeN, free) = markup_elem "free"; +val (skolemN, skolem) = markup_elem "skolem"; +val (boundN, bound) = markup_elem "bound"; +val (varN, var) = markup_elem "var"; +val (numN, num) = markup_elem "num"; +val (xnumN, xnum) = markup_elem "xnum"; +val (xstrN, xstr) = markup_elem "xstr"; -val (sortN, sort) = markup "sort"; -val (typN, typ) = markup "typ"; -val (termN, term) = markup "term"; +val (sortN, sort) = markup_elem "sort"; +val (typN, typ) = markup_elem "typ"; +val (termN, term) = markup_elem "term"; (* outer syntax *) @@ -152,27 +159,37 @@ val command_declN = "command_decl"; fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]); -val (stringN, string) = markup "string"; -val (altstringN, altstring) = markup "altstring"; -val (verbatimN, verbatim) = markup "verbatim"; -val (commentN, comment) = markup "comment"; -val (controlN, control) = markup "control"; -val (malformedN, malformed) = markup "malformed"; +val (stringN, string) = markup_elem "string"; +val (altstringN, altstring) = markup_elem "altstring"; +val (verbatimN, verbatim) = markup_elem "verbatim"; +val (commentN, comment) = markup_elem "comment"; +val (controlN, control) = markup_elem "control"; +val (malformedN, malformed) = markup_elem "malformed"; -val (antiqN, antiq) = markup "antiq"; +val (antiqN, antiq) = markup_elem "antiq"; -val (whitespaceN, whitespace) = markup "whitespace"; -val (junkN, junk) = markup "junk"; +val (whitespaceN, whitespace) = markup_elem "whitespace"; +val (junkN, junk) = markup_elem "junk"; val (commandspanN, commandspan) = markup_string "commandspan" nameN; (* toplevel *) -val (promptN, prompt) = markup "prompt"; -val (stateN, state) = markup "state"; -val (subgoalN, subgoal) = markup "subgoal"; -val (sendbackN, sendback) = markup "sendback"; -val (hiliteN, hilite) = markup "hilite"; +val (promptN, prompt) = markup_elem "prompt"; +val (stateN, state) = markup_elem "state"; +val (subgoalN, subgoal) = markup_elem "subgoal"; +val (sendbackN, sendback) = markup_elem "sendback"; +val (hiliteN, hilite) = markup_elem "hilite"; + + +(* channels *) + +val (writelnN, writeln) = markup_elem "writeln"; +val (priorityN, priority) = markup_elem "priority"; +val (tracingN, tracing) = markup_elem "tracing"; +val (warningN, warning) = markup_elem "warning"; +val (errorN, error) = markup_elem "error"; +val (debugN, debug) = markup_elem "debug"; (* print mode operations *) @@ -194,4 +211,8 @@ val enclose = output #-> Library.enclose; +fun markup m = + let val (bg, en) = output m + in Library.enclose (Output.escape bg) (Output.escape en) end; + end;