# HG changeset patch
# User wenzelm
# Date 1207240961 -7200
# Node ID cd01c8eb314a783e4187cb7a1df3bf676280c7dd
# Parent  ffc1f97ab5fc0b0793b60303c84d5c9584b4b0d0
moved output_markup to xml.ML;
added yxmlN mode name;

diff -r ffc1f97ab5fc -r cd01c8eb314a src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Thu Apr 03 18:42:40 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Thu Apr 03 18:42:41 2008 +0200
@@ -22,7 +22,7 @@
 
 signature ISABELLE_PROCESS =
 sig
-  val output_markup: Markup.T -> output * output
+  val yxmlN: string
   val full_markupN: string
   val test_markupN: string
   val isabelle_processN: string
@@ -34,14 +34,11 @@
 
 (* explicit markup *)
 
-fun output_markup (name, props) =
- (enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
-  enclose "</" ">" name);
-
+val yxmlN = "YXML";
 val full_markupN = "full_markup";
 val test_markupN = "test_markup";
 
-val _ = Markup.add_mode test_markupN output_markup;
+val _ = Markup.add_mode test_markupN XML.output_markup;
 
 
 (* symbol output *)
@@ -86,13 +83,13 @@
 
 val _ = Markup.add_mode isabelle_processN (fn (name, props) =>
   if print_mode_active full_markupN orelse name = Markup.positionN
-  then output_markup (name, props) else ("", ""));
+  then XML.output_markup (name, props) else ("", ""));
 
 fun message ch txt0 =
   let
     val txt1 = XML.element "message" [] [txt0];
     val (txt, pos) =
-      (case try XML.tree_of_string txt1 of
+      (case try XML.parse txt1 of
         NONE => (txt1, Position.none)
       | SOME xml =>
           (if print_mode_active full_markupN then XML.header ^ txt1 else XML.plain_content xml,
@@ -130,7 +127,7 @@
 local
 
 fun markup kind x =
-  ((output_markup (kind, []) |-> enclose) (Output.output x), Symbol.length (Symbol.explode x));
+  ((XML.output_markup (kind, []) |-> enclose) (Output.output x), Symbol.length (Symbol.explode x));
 
 fun free_or_skolem x =
   (case try Name.dest_skolem x of