support "YXML" mode for output transfer notation;
authorwenzelm
Tue Apr 08 11:59:25 2008 +0200 (2008-04-08)
changeset 26574560d07845442
parent 26573 ea36563210cc
child 26575 042617a1c86c
support "YXML" mode for output transfer notation;
tuned;
src/Pure/Tools/isabelle_process.ML
     1.1 --- a/src/Pure/Tools/isabelle_process.ML	Tue Apr 08 09:42:18 2008 +0200
     1.2 +++ b/src/Pure/Tools/isabelle_process.ML	Tue Apr 08 11:59:25 2008 +0200
     1.3 @@ -22,8 +22,9 @@
     1.4  
     1.5  signature ISABELLE_PROCESS =
     1.6  sig
     1.7 +  val isabelle_processN: string
     1.8    val full_markupN: string
     1.9 -  val isabelle_processN: string
    1.10 +  val yxmlN: string
    1.11    val init: unit -> unit
    1.12  end;
    1.13  
    1.14 @@ -34,6 +35,7 @@
    1.15  
    1.16  val isabelle_processN = "isabelle_process";
    1.17  val full_markupN = "full_markup";
    1.18 +val yxmlN = "YXML";
    1.19  
    1.20  val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
    1.21  
    1.22 @@ -50,17 +52,24 @@
    1.23  
    1.24  local
    1.25  
    1.26 +fun clean_string bad str =
    1.27 +  if exists_string (member (op =) bad) str then
    1.28 +    translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
    1.29 +  else str;
    1.30 +
    1.31  fun message_props props =
    1.32 -  let
    1.33 -    val clean = translate_string (fn c =>
    1.34 -      if c = Symbol.STX orelse c = "\n" orelse c = "\r" then Symbol.DEL else c);
    1.35 +  let val clean = clean_string [Symbol.STX, "\n", "\r"]
    1.36    in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
    1.37  
    1.38  fun message_text ts =
    1.39 -  (if print_mode_active full_markupN
    1.40 -    then XML.header ^ XML.string_of (XML.Elem ("message", [], ts))
    1.41 -    else Buffer.content (fold XML.add_content ts Buffer.empty))
    1.42 -  |> translate_string (fn c => if c = Symbol.STX then Symbol.DEL else c);
    1.43 +  let
    1.44 +    val doc = XML.Elem ("message", [], ts);
    1.45 +    val msg =
    1.46 +      if not (print_mode_active full_markupN) then
    1.47 +        Buffer.content (fold XML.add_content ts Buffer.empty)
    1.48 +      else if print_mode_active yxmlN then YXML.string_of doc
    1.49 +      else XML.header ^ XML.string_of doc;
    1.50 +  in clean_string [Symbol.STX] msg end;
    1.51  
    1.52  fun message_pos ts = get_first get_pos ts
    1.53  and get_pos (elem as XML.Elem (name, atts, ts)) =