moved output_markup to xml.ML;
authorwenzelm
Thu Apr 03 18:42:41 2008 +0200 (2008-04-03)
changeset 26543cd01c8eb314a
parent 26542 ffc1f97ab5fc
child 26544 af4c77a21c06
moved output_markup to xml.ML;
added yxmlN mode name;
src/Pure/Tools/isabelle_process.ML
     1.1 --- a/src/Pure/Tools/isabelle_process.ML	Thu Apr 03 18:42:40 2008 +0200
     1.2 +++ b/src/Pure/Tools/isabelle_process.ML	Thu Apr 03 18:42:41 2008 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  
     1.5  signature ISABELLE_PROCESS =
     1.6  sig
     1.7 -  val output_markup: Markup.T -> output * output
     1.8 +  val yxmlN: string
     1.9    val full_markupN: string
    1.10    val test_markupN: string
    1.11    val isabelle_processN: string
    1.12 @@ -34,14 +34,11 @@
    1.13  
    1.14  (* explicit markup *)
    1.15  
    1.16 -fun output_markup (name, props) =
    1.17 - (enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
    1.18 -  enclose "</" ">" name);
    1.19 -
    1.20 +val yxmlN = "YXML";
    1.21  val full_markupN = "full_markup";
    1.22  val test_markupN = "test_markup";
    1.23  
    1.24 -val _ = Markup.add_mode test_markupN output_markup;
    1.25 +val _ = Markup.add_mode test_markupN XML.output_markup;
    1.26  
    1.27  
    1.28  (* symbol output *)
    1.29 @@ -86,13 +83,13 @@
    1.30  
    1.31  val _ = Markup.add_mode isabelle_processN (fn (name, props) =>
    1.32    if print_mode_active full_markupN orelse name = Markup.positionN
    1.33 -  then output_markup (name, props) else ("", ""));
    1.34 +  then XML.output_markup (name, props) else ("", ""));
    1.35  
    1.36  fun message ch txt0 =
    1.37    let
    1.38      val txt1 = XML.element "message" [] [txt0];
    1.39      val (txt, pos) =
    1.40 -      (case try XML.tree_of_string txt1 of
    1.41 +      (case try XML.parse txt1 of
    1.42          NONE => (txt1, Position.none)
    1.43        | SOME xml =>
    1.44            (if print_mode_active full_markupN then XML.header ^ txt1 else XML.plain_content xml,
    1.45 @@ -130,7 +127,7 @@
    1.46  local
    1.47  
    1.48  fun markup kind x =
    1.49 -  ((output_markup (kind, []) |-> enclose) (Output.output x), Symbol.length (Symbol.explode x));
    1.50 +  ((XML.output_markup (kind, []) |-> enclose) (Output.output x), Symbol.length (Symbol.explode x));
    1.51  
    1.52  fun free_or_skolem x =
    1.53    (case try Name.dest_skolem x of