# HG changeset patch # User wenzelm # Date 1232142972 -3600 # Node ID 793766d4c1b5d13532f5d5a200d3e3294885ee59 # Parent 736bf7117153ae162af69270ceea01257ae0229d moved message markup into Scala layer -- reduced redundancy; diff -r 736bf7117153 -r 793766d4c1b5 src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Fri Jan 16 22:54:11 2009 +0100 +++ b/src/Pure/General/markup.ML Fri Jan 16 22:56:12 2009 +0100 @@ -95,17 +95,7 @@ val editN: string val edit: string -> string -> T val pidN: string val sessionN: string - val classN: string - val messageN: string val message: string -> T val promptN: string val prompt: T - val writelnN: string - val priorityN: string - val tracingN: string - val warningN: string - val errorN: string - val debugN: string - val initN: string - val statusN: string val no_output: output * output val default_output: T -> output * output val add_mode: string -> (T -> output * output) -> unit @@ -284,19 +274,8 @@ val pidN = "pid"; val sessionN = "session"; -val classN = "class"; -val (messageN, message) = markup_string "message" classN; - val (promptN, prompt) = markup_elem "prompt"; -val writelnN = "writeln"; -val priorityN = "priority"; -val tracingN = "tracing"; -val warningN = "warning"; -val errorN = "error"; -val debugN = "debug"; -val initN = "init"; -val statusN = "status"; (* print mode operations *) diff -r 736bf7117153 -r 793766d4c1b5 src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Fri Jan 16 22:54:11 2009 +0100 +++ b/src/Pure/General/markup.scala Fri Jan 16 22:56:12 2009 +0100 @@ -131,6 +131,21 @@ val SESSION = "session" val MESSAGE = "message" + val CLASS = "class" + + val INIT = "init" + val STATUS = "status" + val WRITELN = "writeln" + val PRIORITY = "priority" + val TRACING = "tracing" + val WARNING = "warning" + val ERROR = "error" + val DEBUG = "debug" + val SYSTEM = "system" + val STDIN = "stdin" + val STDOUT = "stdout" + val SIGNAL = "signal" + val EXIT = "exit" /* content */ diff -r 736bf7117153 -r 793766d4c1b5 src/Pure/Tools/isabelle_process.ML --- a/src/Pure/Tools/isabelle_process.ML Fri Jan 16 22:54:11 2009 +0100 +++ b/src/Pure/Tools/isabelle_process.ML Fri Jan 16 22:56:12 2009 +0100 @@ -55,9 +55,6 @@ let val clean = clean_string [Symbol.STX, "\n", "\r"] in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end; -fun message_text class body = - YXML.element Markup.messageN [(Markup.classN, class)] [clean_string [Symbol.STX] body]; - fun message_pos trees = trees |> get_first (fn XML.Elem (name, atts, ts) => if name = Markup.positionN then SOME (Position.of_properties atts) @@ -69,21 +66,21 @@ in -fun message _ _ _ "" = () - | message out_stream ch class body = +fun message _ _ "" = () + | message out_stream ch body = let val pos = the_default Position.none (message_pos (YXML.parse_body body)); val props = Position.properties_of (Position.thread_data ()) |> Position.default_properties pos; - val txt = message_text class body; + val txt = clean_string [Symbol.STX] body; in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end; fun init_message out_stream = let val pid = (Markup.pidN, process_id ()); val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown"); - val text = message_text Markup.initN (Session.welcome ()); + val text = Session.welcome (); in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end; end; @@ -116,13 +113,13 @@ val _ = SimpleThread.fork false (auto_flush out_stream); val _ = SimpleThread.fork false (auto_flush TextIO.stdErr); in - Output.status_fn := message out_stream "B" Markup.statusN; - Output.writeln_fn := message out_stream "C" Markup.writelnN; - Output.priority_fn := message out_stream "D" Markup.priorityN; - Output.tracing_fn := message out_stream "E" Markup.tracingN; - Output.warning_fn := message out_stream "F" Markup.warningN; - Output.error_fn := message out_stream "G" Markup.errorN; - Output.debug_fn := message out_stream "H" Markup.debugN; + Output.status_fn := message out_stream "B"; + Output.writeln_fn := message out_stream "C"; + Output.priority_fn := message out_stream "D"; + Output.tracing_fn := message out_stream "E"; + Output.warning_fn := message out_stream "F"; + Output.error_fn := message out_stream "G"; + Output.debug_fn := message out_stream "H"; Output.prompt_fn := ignore; out_stream end; diff -r 736bf7117153 -r 793766d4c1b5 src/Pure/Tools/isabelle_process.scala --- a/src/Pure/Tools/isabelle_process.scala Fri Jan 16 22:54:11 2009 +0100 +++ b/src/Pure/Tools/isabelle_process.scala Fri Jan 16 22:56:12 2009 +0100 @@ -50,6 +50,21 @@ ('2' : Int) -> Kind.STDOUT, ('3' : Int) -> Kind.SIGNAL, ('4' : Int) -> Kind.EXIT) + // message markup + val markup = Map( + Kind.INIT -> Markup.INIT, + Kind.STATUS -> Markup.STATUS, + Kind.WRITELN -> Markup.WRITELN, + Kind.PRIORITY -> Markup.PRIORITY, + Kind.TRACING -> Markup.TRACING, + Kind.WARNING -> Markup.WARNING, + Kind.ERROR -> Markup.ERROR, + Kind.DEBUG -> Markup.DEBUG, + Kind.SYSTEM -> Markup.SYSTEM, + Kind.STDIN -> Markup.STDIN, + Kind.STDOUT -> Markup.STDOUT, + Kind.SIGNAL -> Markup.SIGNAL, + Kind.EXIT -> Markup.EXIT) //}}} def is_raw(kind: Value) = kind == STDOUT @@ -67,8 +82,10 @@ class Result(val kind: Kind.Value, val props: Properties, val result: String) { override def toString = { - val tree = YXML.parse_failsafe(result) - val res = if (kind == Kind.STATUS) tree.toString else XML.content(tree).mkString + val trees = YXML.parse_body_failsafe(result) + val res = + if (kind == Kind.STATUS) trees.map(_.toString).mkString + else trees.flatMap(XML.content(_).mkString).mkString if (props == null) kind.toString + " [[" + res + "]]" else kind.toString + " " + props.toString + " [[" + res + "]]" } @@ -77,6 +94,10 @@ def is_system = Kind.is_system(kind) } + def parse_message(kind: Kind.Value, result: String) = { + XML.Elem(Markup.MESSAGE, List((Markup.CLASS, Kind.markup(kind))), + YXML.parse_body_failsafe(result)) + } }