removed yxmlN for now;
authorwenzelm
Thu Apr 03 21:23:42 2008 +0200 (2008-04-03)
changeset 26550a8740ad422d2
parent 26549 9838e45c6e6c
child 26551 da1cd11d8a25
removed yxmlN for now;
moved test_markup to proof_general_emacs.ML;
use efficient YXML markup internally (output, markup, message);
message: issue MALFORMED MESSAGE explicitly;
tuned;
src/Pure/Tools/isabelle_process.ML
     1.1 --- a/src/Pure/Tools/isabelle_process.ML	Thu Apr 03 21:23:41 2008 +0200
     1.2 +++ b/src/Pure/Tools/isabelle_process.ML	Thu Apr 03 21:23:42 2008 +0200
     1.3 @@ -22,9 +22,7 @@
     1.4  
     1.5  signature ISABELLE_PROCESS =
     1.6  sig
     1.7 -  val yxmlN: string
     1.8    val full_markupN: string
     1.9 -  val test_markupN: string
    1.10    val isabelle_processN: string
    1.11    val init: unit -> unit
    1.12  end;
    1.13 @@ -32,32 +30,16 @@
    1.14  structure IsabelleProcess: ISABELLE_PROCESS =
    1.15  struct
    1.16  
    1.17 -(* explicit markup *)
    1.18 -
    1.19 -val yxmlN = "YXML";
    1.20 -val full_markupN = "full_markup";
    1.21 -val test_markupN = "test_markup";
    1.22 -
    1.23 -val _ = Markup.add_mode test_markupN XML.output_markup;
    1.24 -
    1.25 -
    1.26 -(* symbol output *)
    1.27 +(* print modes *)
    1.28  
    1.29  val isabelle_processN = "isabelle_process";
    1.30 +val full_markupN = "full_markup";
    1.31  
    1.32 -local
    1.33 +val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
    1.34  
    1.35 -fun output str =
    1.36 -  let
    1.37 -    fun out s = if Symbol.is_raw s then Symbol.decode_raw s else XML.text s;
    1.38 -    val syms = Symbol.explode str;
    1.39 -  in (implode (map out syms), Symbol.length syms) end;
    1.40 -
    1.41 -in
    1.42 -
    1.43 -val _ = Output.add_mode isabelle_processN output Symbol.encode_raw;
    1.44 -
    1.45 -end;
    1.46 +val _ = Markup.add_mode isabelle_processN (fn (name, props) =>
    1.47 +  if print_mode_active full_markupN orelse name = Markup.positionN
    1.48 +  then YXML.output_markup (name, props) else ("", ""));
    1.49  
    1.50  
    1.51  (* message markup *)
    1.52 @@ -68,44 +50,43 @@
    1.53  
    1.54  local
    1.55  
    1.56 -fun print_props props =
    1.57 +fun message_props props =
    1.58    let
    1.59      val clean = translate_string (fn c =>
    1.60        if c = Symbol.STX orelse c = "\n" orelse c = "\r" then Symbol.DEL else c);
    1.61    in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
    1.62  
    1.63 -fun get_pos (elem as XML.Elem (name, atts, ts)) =
    1.64 +fun message_text ts =
    1.65 +  (if print_mode_active full_markupN
    1.66 +    then XML.header ^ XML.string_of (XML.Elem ("message", [], ts))
    1.67 +    else Buffer.content (fold XML.add_content ts Buffer.empty))
    1.68 +  |> translate_string (fn c => if c = Symbol.STX then Symbol.DEL else c);
    1.69 +
    1.70 +fun message_pos ts = get_first get_pos ts
    1.71 +and get_pos (elem as XML.Elem (name, atts, ts)) =
    1.72        if name = Markup.positionN then SOME (Position.of_properties atts)
    1.73 -      else get_first get_pos ts
    1.74 -  | get_pos _ = NONE;
    1.75 +      else message_pos ts
    1.76 +  | get_pos _ = NONE
    1.77  
    1.78  in
    1.79  
    1.80 -val _ = Markup.add_mode isabelle_processN (fn (name, props) =>
    1.81 -  if print_mode_active full_markupN orelse name = Markup.positionN
    1.82 -  then XML.output_markup (name, props) else ("", ""));
    1.83 -
    1.84 -fun message ch txt0 =
    1.85 +fun message ch body =
    1.86    let
    1.87 -    val txt1 = XML.element "message" [] [txt0];
    1.88      val (txt, pos) =
    1.89 -      (case try XML.parse txt1 of
    1.90 -        NONE => (txt1, Position.none)
    1.91 -      | SOME xml =>
    1.92 -          (if print_mode_active full_markupN then XML.header ^ txt1 else XML.plain_content xml,
    1.93 -            the_default Position.none (get_pos xml)))
    1.94 -      |>> translate_string (fn c => if c = Symbol.STX then Symbol.DEL else c);
    1.95 +      let val ts = YXML.parse_body body
    1.96 +      in (message_text ts, the_default Position.none (message_pos ts)) end
    1.97 +      handle Fail msg => ("*** MALFORMED MESSAGE ***\n" ^ msg, Position.none);
    1.98      val props =
    1.99        Position.properties_of (Position.thread_data ())
   1.100        |> Position.default_properties pos;
   1.101 -  in Output.writeln_default (special ch ^ print_props props ^ txt ^ special_end) end;
   1.102 +  in Output.writeln_default (special ch ^ message_props props ^ txt ^ special_end) end;
   1.103  
   1.104  fun init_message () =
   1.105    let
   1.106      val pid = ("pid", string_of_pid (Posix.ProcEnv.getpid ()));
   1.107      val session = ("session", List.last (Session.id ()) handle List.Empty => "unknown");
   1.108      val welcome = Session.welcome ();
   1.109 -  in Output.writeln_default (special "H" ^ print_props [pid, session] ^ welcome ^ special_end) end;
   1.110 +  in Output.writeln_default (special "H" ^ message_props [pid, session] ^ welcome ^ special_end) end;
   1.111  
   1.112  end;
   1.113  
   1.114 @@ -127,7 +108,7 @@
   1.115  local
   1.116  
   1.117  fun markup kind x =
   1.118 -  ((XML.output_markup (kind, []) |-> enclose) (Output.output x), Symbol.length (Symbol.explode x));
   1.119 +  ((YXML.output_markup (kind, []) |-> enclose) (Output.output x), Symbol.length (Symbol.explode x));
   1.120  
   1.121  fun free_or_skolem x =
   1.122    (case try Name.dest_skolem x of