# HG changeset patch
# User wenzelm
# Date 1230935795 -3600
# Node ID dc2663942cccf6890a089da41edb8157c535d496
# Parent  e02b3a32f34f22135257094427a4e0c346a153f1# Parent  eba7f9f3b06dbeebf33ab0ae87ce5bff6a5f093b
merged

diff -r e02b3a32f34f -r dc2663942ccc lib/html/isabelle.css
--- a/lib/html/isabelle.css	Fri Jan 02 22:06:56 2009 +0100
+++ b/lib/html/isabelle.css	Fri Jan 02 23:36:35 2009 +0100
@@ -20,20 +20,20 @@
 
 /* inner and outer syntax markup */
 
-.tfree, tfree          { color: purple; }
-.tvar, tvar            { color: purple; }
-.free, free            { color: blue; }
-.skolem, skolem        { color: brown; }
-.bound, bound          { color: green; }
-.var, var              { color: blue; }
-.num, num              { }
-.xnum, xnum            { }
-.xstr, xstr            { color: brown; }
-.literal, literal      { font-weight: bold; }
-                      
+.tfree, tfree                 { color: purple; }
+.tvar, tvar                   { color: purple; }
+.free, free                   { color: blue; }
+.skolem, skolem               { color: brown; }
+.bound, bound                 { color: green; }
+.var, var                     { color: blue; }
+.numeral, numeral             { }
+.literal, literal             { font-weight: bold; }
+.inner_string, inner_string   { color: brown; }
+.inner_comment, inner_comment { color: #8B0000; }
+
 .loc, loc              { color: brown; }
 .tclass, tclass        { color: red; }
-          
+
 .keyword, keyword      { font-weight: bold; }
 .command, command      { font-weight: bold; }
 .ident, ident          { }
diff -r e02b3a32f34f -r dc2663942ccc src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/numeral_syntax.ML
-    ID:         $Id$
     Authors:    Markus Wenzel, TU Muenchen
 
 Concrete syntax for generic numerals -- preserves leading zeros/ones.
@@ -19,12 +18,11 @@
 
 fun mk_bin num =
   let
-    val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
     fun bit b bs = HOLogic.mk_bit b $ bs;
-    fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Int.Pls})
-      | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Int.Min})
+    fun mk 0 = Syntax.const @{const_name Int.Pls}
+      | mk ~1 = Syntax.const @{const_name Int.Min}
       | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
-  in mk value end;
+  in mk (#value (Syntax.read_xnum num)) end;
 
 in
 
@@ -65,15 +63,18 @@
     else sign ^ implode (replicate z "0") ^ num
   end;
 
+fun syntax_numeral t =
+  Syntax.const "_Numeral" $ (Syntax.const "_numeral" $ Syntax.free (dest_bin_str t));
+
 in
 
 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
-      let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
-        if not (! show_types) andalso can Term.dest_Type T then t'
-        else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
-      end
+      let val t' =
+        if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
+        else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
+      in list_comb (t', ts) end
   | numeral_tr' _ (*"number_of"*) T (t :: ts) =
-      if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t)
+      if T = dummyT then list_comb (syntax_numeral t, ts)
       else raise Match
   | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
 
diff -r e02b3a32f34f -r dc2663942ccc src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/HOL/Tools/string_syntax.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/string_syntax.ML
-    ID:         $Id$
     Author:     Makarius
 
 Concrete syntax for hex chars and strings.
@@ -43,8 +42,8 @@
 fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
   | dest_char _ = raise Match;
 
-fun syntax_xstr cs =
-  Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)];
+fun syntax_string cs =
+  Syntax.Appl [Syntax.Constant "_inner_string", Syntax.Variable (Syntax.implode_xstr cs)];
 
 
 fun char_ast_tr [Syntax.Variable xstr] =
@@ -53,7 +52,7 @@
     | _ => error ("Single character expected: " ^ xstr))
   | char_ast_tr asts = raise AST ("char_ast_tr", asts);
 
-fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_xstr [dest_chr c1 c2]]
+fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_string [dest_chr c1 c2]]
   | char_ast_tr' _ = raise Match;
 
 
@@ -70,7 +69,7 @@
   | string_ast_tr asts = raise AST ("string_tr", asts);
 
 fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
-        syntax_xstr (map dest_char (Syntax.unfold_ast "_args" args))]
+        syntax_string (map dest_char (Syntax.unfold_ast "_args" args))]
   | list_ast_tr' ts = raise Match;
 
 
diff -r e02b3a32f34f -r dc2663942ccc src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/HOLCF/Fixrec.thy	Fri Jan 02 23:36:35 2009 +0100
@@ -216,19 +216,19 @@
 
 syntax
   "_pat" :: "'a"
-  "_var" :: "'a"
+  "_variable" :: "'a"
   "_noargs" :: "'a"
 
 translations
-  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_var p r)"
-  "_var (_args x y) r" => "CONST csplit\<cdot>(_var x (_var y r))"
-  "_var _noargs r" => "CONST unit_when\<cdot>r"
+  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_variable p r)"
+  "_variable (_args x y) r" => "CONST csplit\<cdot>(_variable x (_variable y r))"
+  "_variable _noargs r" => "CONST unit_when\<cdot>r"
 
 parse_translation {*
 (* rewrites (_pat x) => (return) *)
-(* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
+(* rewrites (_variable x t) => (Abs_CFun (%x. t)) *)
   [("_pat", K (Syntax.const "Fixrec.return")),
-   mk_binder_tr ("_var", "Abs_CFun")];
+   mk_binder_tr ("_variable", "Abs_CFun")];
 *}
 
 text {* Printing Case expressions *}
@@ -250,7 +250,7 @@
             val abs = case t of Abs abs => abs
                 | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
             val (x, t') = atomic_abs_tr' abs;
-          in (Syntax.const "_var" $ x, t') end
+          in (Syntax.const "_variable" $ x, t') end
     |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
 
     fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
@@ -261,7 +261,7 @@
 *}
 
 translations
-  "x" <= "_match Fixrec.return (_var x)"
+  "x" <= "_match Fixrec.return (_variable x)"
 
 
 subsection {* Pattern combinators for data constructors *}
@@ -320,18 +320,18 @@
 
 text {* Parse translations (variables) *}
 translations
-  "_var (XCONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
-  "_var (XCONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
-  "_var (XCONST sinl\<cdot>x) r" => "_var x r"
-  "_var (XCONST sinr\<cdot>x) r" => "_var x r"
-  "_var (XCONST up\<cdot>x) r" => "_var x r"
-  "_var (XCONST TT) r" => "_var _noargs r"
-  "_var (XCONST FF) r" => "_var _noargs r"
-  "_var (XCONST ONE) r" => "_var _noargs r"
+  "_variable (XCONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
+  "_variable (XCONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
+  "_variable (XCONST sinl\<cdot>x) r" => "_variable x r"
+  "_variable (XCONST sinr\<cdot>x) r" => "_variable x r"
+  "_variable (XCONST up\<cdot>x) r" => "_variable x r"
+  "_variable (XCONST TT) r" => "_variable _noargs r"
+  "_variable (XCONST FF) r" => "_variable _noargs r"
+  "_variable (XCONST ONE) r" => "_variable _noargs r"
 
 translations
-  "_var (CONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
-  "_var (CONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
+  "_variable (CONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
+  "_variable (CONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
 
 text {* Print translations *}
 translations
@@ -437,14 +437,14 @@
 
 text {* Parse translations (variables) *}
 translations
-  "_var _ r" => "_var _noargs r"
-  "_var (_as_pat x y) r" => "_var (_args x y) r"
-  "_var (_lazy_pat x) r" => "_var x r"
+  "_variable _ r" => "_variable _noargs r"
+  "_variable (_as_pat x y) r" => "_variable (_args x y) r"
+  "_variable (_lazy_pat x) r" => "_variable x r"
 
 text {* Print translations *}
 translations
   "_" <= "_match (CONST wild_pat) _noargs"
-  "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_var x) v)"
+  "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_variable x) v)"
   "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
 
 text {* Lazy patterns in lambda abstractions *}
diff -r e02b3a32f34f -r dc2663942ccc src/HOLCF/Tools/domain/domain_syntax.ML
--- a/src/HOLCF/Tools/domain/domain_syntax.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -89,7 +89,7 @@
     fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
     fun when1 n m = if n = m then arg1 n else K (Constant "UU");
 
-    fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"];
+    fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
     fun app_pat x = mk_appl (Constant "_pat") [x];
     fun args_list [] = Constant "_noargs"
     |   args_list xs = foldr1 (app "_args") xs;
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/General/buffer.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/buffer.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Efficient text buffers.
@@ -10,7 +9,6 @@
   type T
   val empty: T
   val add: string -> T -> T
-  val add_substring: substring -> T -> T
   val markup: Markup.T -> (T -> T) -> T -> T
   val content: T -> string
   val output: T -> TextIO.outstream -> unit
@@ -19,46 +17,18 @@
 structure Buffer: BUFFER =
 struct
 
-(* datatype *)
-
-datatype T =
-    EmptyBuffer
-  | String of string * T
-  | Substring of substring * T;
+datatype T = Buffer of string list;
 
-val empty = EmptyBuffer;
-
+val empty = Buffer [];
 
-(* add content *)
-
-fun add s buf = if s = "" then buf else String (s, buf);
-fun add_substring s buf = if Substring.isEmpty s then buf else Substring (s, buf);
+fun add "" buf = buf
+  | add x (Buffer xs) = Buffer (x :: xs);
 
 fun markup m body =
   let val (bg, en) = Markup.output m
   in add bg #> body #> add en end;
 
-
-(* cumulative content *)
-
-fun rev_content EmptyBuffer acc = acc
-  | rev_content (String (s, buf)) acc = rev_content buf (s :: acc)
-  | rev_content (Substring (s, buf)) acc = rev_content buf (Substring.string s :: acc);
-
-fun content buf = implode (rev_content buf []);
-
-
-(* file output *)
-
-fun rev_buffer EmptyBuffer acc = acc
-  | rev_buffer (String (s, buf)) acc = rev_buffer buf (String (s, acc))
-  | rev_buffer (Substring (s, buf)) acc = rev_buffer buf (Substring (s, acc));
-
-fun output buffer stream =
-  let
-    fun rev_output EmptyBuffer = ()
-      | rev_output (String (s, buf)) = (TextIO.output (stream, s); rev_output buf)
-      | rev_output (Substring (s, buf)) = (TextIO.outputSubstr (stream, s); rev_output buf);
-  in rev_output (rev_buffer buffer empty) end;
+fun content (Buffer xs) = implode (rev xs);
+fun output (Buffer xs) stream = List.app (fn s => TextIO.output (stream, s)) (rev xs);
 
 end;
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/General/markup.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/markup.ML
-    ID:         $Id$
     Author:     Makarius
 
 Common markup elements.
@@ -52,11 +51,9 @@
   val skolemN: string val skolem: T
   val boundN: string val bound: T
   val varN: string val var: T
-  val numN: string val num: T
-  val floatN: string val float: T
-  val xnumN: string val xnum: T
-  val xstrN: string val xstr: T
+  val numeralN: string val numeral: T
   val literalN: string val literal: T
+  val inner_stringN: string val inner_string: T
   val inner_commentN: string val inner_comment: T
   val sortN: string val sort: T
   val typN: string val typ: T
@@ -106,6 +103,7 @@
   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
   val output: T -> output * output
@@ -203,11 +201,9 @@
 val (skolemN, skolem) = markup_elem "skolem";
 val (boundN, bound) = markup_elem "bound";
 val (varN, var) = markup_elem "var";
-val (numN, num) = markup_elem "num";
-val (floatN, float) = markup_elem "float";
-val (xnumN, xnum) = markup_elem "xnum";
-val (xstrN, xstr) = markup_elem "xstr";
+val (numeralN, numeral) = markup_elem "numeral";
 val (literalN, literal) = markup_elem "literal";
+val (inner_stringN, inner_string) = markup_elem "inner_string";
 val (inner_commentN, inner_comment) = markup_elem "inner_comment";
 
 val (sortN, sort) = markup_elem "sort";
@@ -292,7 +288,8 @@
 
 (* print mode operations *)
 
-fun default_output (_: T) = ("", "");
+val no_output = ("", "");
+fun default_output (_: T) = no_output;
 
 local
   val default = {output = default_output};
@@ -304,7 +301,7 @@
     the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
 
-fun output m = if is_none m then ("", "") else #output (get_mode ()) m;
+fun output m = if is_none m then no_output else #output (get_mode ()) m;
 
 val enclose = output #-> Library.enclose;
 
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/General/symbol.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -65,6 +65,7 @@
   val bump_string: string -> string
   val length: symbol list -> int
   val xsymbolsN: string
+  val output: string -> output * int
 end;
 
 structure Symbol: SYMBOL =
@@ -175,21 +176,22 @@
   ord space <= ord c andalso ord c <= ord "~" andalso c <> "." andalso c <> ">"
   orelse ord c >= 128;
 
-fun encode_raw str =
-  let
-    val raw0 = enclose "\\<^raw:" ">";
-    val raw1 = raw0 o implode;
-    val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
-
-    fun encode cs = enc (Library.take_prefix raw_chr cs)
-    and enc ([], []) = []
-      | enc (cs, []) = [raw1 cs]
-      | enc ([], d :: ds) = raw2 d :: encode ds
-      | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
-  in
-    if exists_string (not o raw_chr) str then implode (encode (explode str))
-    else raw0 str
-  end;
+fun encode_raw "" = ""
+  | encode_raw str =
+      let
+        val raw0 = enclose "\\<^raw:" ">";
+        val raw1 = raw0 o implode;
+        val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
+    
+        fun encode cs = enc (Library.take_prefix raw_chr cs)
+        and enc ([], []) = []
+          | enc (cs, []) = [raw1 cs]
+          | enc ([], d :: ds) = raw2 d :: encode ds
+          | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
+      in
+        if exists_string (not o raw_chr) str then implode (encode (explode str))
+        else raw0 str
+      end;
 
 
 (* diagnostics *)
@@ -519,9 +521,9 @@
 
 
 
-(** xsymbols **)
+(** symbol output **)
 
-val xsymbolsN = "xsymbols";
+(* length *)
 
 fun sym_len s =
   if not (is_printable s) then (0: int)
@@ -532,8 +534,16 @@
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
 
+
+(* print mode *)
+
+val xsymbolsN = "xsymbols";
+
+fun output s = (s, sym_length (sym_explode s));
+
+
 (*final declarations of this structure!*)
+val explode = sym_explode;
 val length = sym_length;
-val explode = sym_explode;
 
 end;
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/General/xml.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -79,7 +79,7 @@
   end;
 
 fun output_markup (markup as (name, atts)) =
-  if Markup.is_none markup then ("", "")
+  if Markup.is_none markup then Markup.no_output
   else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
 
 
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/General/yxml.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -42,7 +42,7 @@
 (* output *)
 
 fun output_markup (markup as (name, atts)) =
-  if Markup.is_none markup then ("", "")
+  if Markup.is_none markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
 fun element name atts body =
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -408,9 +408,8 @@
    ("free", free_or_skolem),
    ("bound", plain_markup Markup.bound),
    ("var", var_or_skolem),
-   ("num", plain_markup Markup.num),
-   ("xnum", plain_markup Markup.xnum),
-   ("xstr", plain_markup Markup.xstr)];
+   ("numeral", plain_markup Markup.numeral),
+   ("inner_string", plain_markup Markup.inner_string)];
 
 in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end;
 
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/proof_general_emacs.ML
-    ID:         $Id$
     Author:     David Aspinall and Markus Wenzel
 
 Isabelle/Isar configuration for Emacs Proof General.
@@ -21,81 +20,77 @@
 (* print modes *)
 
 val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
-val pgasciiN = "PGASCII";                  (*plain 7-bit ASCII communication*)
 val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
 val test_markupN = "test_markup";          (*XML markup for everything*)
 
-val _ = Markup.add_mode test_markupN (fn (name, props) =>
-  if name = Markup.promptN then ("", "") else XML.output_markup (name, props));
-
-fun special oct =
-  if print_mode_active pgasciiN then Symbol.SOH ^ chr (ord (oct_char oct) - 167)
-  else oct_char oct;
+fun special ch = Symbol.SOH ^ ch;
 
 
-(* text output: print modes for xsymbol *)
+(* render markup *)
 
 local
 
-fun xsym_output "\\" = "\\\\"
-  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
-
-fun xsymbols_output s =
-  if print_mode_active Symbol.xsymbolsN andalso exists_string (fn c => c = "\\") s then
-    let val syms = Symbol.explode s
-    in (implode (map xsym_output syms), Symbol.length syms) end
-  else Output.default_output s;
+fun render_trees ts = fold render_tree ts
+and render_tree (XML.Text s) = Buffer.add s
+  | render_tree (XML.Elem (name, props, ts)) =
+      let
+        val (bg1, en1) =
+          if name <> Markup.promptN andalso print_mode_active test_markupN
+          then XML.output_markup (name, props)
+          else Markup.no_output;
+        val (bg2, en2) =
+          if (case ts of [XML.Text _] => false | _ => true) then Markup.no_output
+          else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
+          else if name = Markup.sendbackN then (special "W", special "X")
+          else if name = Markup.hiliteN then (special "0", special "1")
+          else if name = Markup.tclassN then (special "B", special "A")
+          else if name = Markup.tfreeN then (special "C", special "A")
+          else if name = Markup.tvarN then (special "D", special "A")
+          else if name = Markup.freeN then (special "E", special "A")
+          else if name = Markup.boundN then (special "F", special "A")
+          else if name = Markup.varN then (special "G", special "A")
+          else if name = Markup.skolemN then (special "H", special "A")
+          else Markup.no_output;
+      in
+        Buffer.add bg1 #>
+        Buffer.add bg2 #>
+        render_trees ts #>
+        Buffer.add en2 #>
+        Buffer.add en1
+      end;
 
 in
 
-fun setup_xsymbols_output () =
-  Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
+fun render text =
+  Buffer.content (render_trees (YXML.parse_body text) Buffer.empty);
 
 end;
 
 
-(* common markup *)
+(* messages *)
+
+fun message bg en prfx text =
+  (case render text of
+    "" => ()
+  | s => Output.writeln_default (enclose bg en (prefix_lines prfx s)));
 
-val _ = Markup.add_mode proof_generalN (fn (name, props) =>
-  let
-    val (bg1, en1) =
-      if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
-      else if name = Markup.sendbackN then (special "376", special "377")
-      else if name = Markup.hiliteN then (special "327", special "330")
-      else if name = Markup.tclassN then (special "351", special "350")
-      else if name = Markup.tfreeN then (special "352", special "350")
-      else if name = Markup.tvarN then (special "353", special "350")
-      else if name = Markup.freeN then (special "354", special "350")
-      else if name = Markup.boundN then (special "355", special "350")
-      else if name = Markup.varN then (special "356", special "350")
-      else if name = Markup.skolemN then (special "357", special "350")
-      else ("", "");
-    val (bg2, en2) =
-      if name <> Markup.promptN andalso print_mode_active test_markupN
-      then XML.output_markup (name, props)
-      else ("", "");
-  in (bg1 ^ bg2, en2 ^ en1) end);
+fun setup_messages () =
+ (Output.writeln_fn := message "" "" "";
+  Output.status_fn := (fn s => ! Output.priority_fn s);
+  Output.priority_fn := message (special "I") (special "J") "";
+  Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
+  Output.debug_fn := message (special "K") (special "L") "+++ ";
+  Output.warning_fn := message (special "K") (special "L") "### ";
+  Output.error_fn := message (special "M") (special "N") "*** ";
+  Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));
+
+fun panic s =
+  (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
 
 
-(* messages and notification *)
-
-fun decorate bg en prfx =
-  Output.writeln_default o enclose bg en o prefix_lines prfx;
+(* notification *)
 
-fun setup_messages () =
- (Output.writeln_fn := Output.writeln_default;
-  Output.status_fn := (fn "" => () | s => ! Output.priority_fn s);
-  Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
-  Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
-  Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
-  Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
-  Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s);
-  Output.prompt_fn := (fn s => Output.std_output (s ^ special "372")));
-
-fun panic s =
-  (decorate (special "364") (special "365") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
-
-fun emacs_notify s = decorate (special "360") (special "361") "" s;
+val emacs_notify = message (special "I") (special "J") "";
 
 fun tell_clear_goals () =
   emacs_notify "Proof General, please clear the goals buffer.";
@@ -237,7 +232,9 @@
   | init true =
       (! initialized orelse
         (Output.no_warnings init_outer_syntax ();
-          setup_xsymbols_output ();
+          Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
+          Output.add_mode proof_generalN Output.default_output Output.default_escape;
+          Markup.add_mode proof_generalN YXML.output_markup;
           setup_messages ();
           ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
           setup_thy_loader ();
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -169,10 +169,10 @@
   | VarSy       => Markup.var
   | TFreeSy     => Markup.tfree
   | TVarSy      => Markup.tvar
-  | NumSy       => Markup.num
-  | FloatSy     => Markup.float
-  | XNumSy      => Markup.xnum
-  | StrSy       => Markup.xstr
+  | NumSy       => Markup.numeral
+  | FloatSy     => Markup.numeral
+  | XNumSy      => Markup.numeral
+  | StrSy       => Markup.inner_string
   | Space       => Markup.none
   | Comment     => Markup.inner_comment
   | EOF         => Markup.none;
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -379,7 +379,7 @@
 
 fun stamp_trfun s (c, f) = (c, (f, s));
 fun mk_trfun tr = stamp_trfun (stamp ()) tr;
-fun eq_trfun ((_, s1:stamp), (_, s2)) = s1 = s2;
+fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
 
 
 (* token translations *)
@@ -387,7 +387,7 @@
 fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
 
 val standard_token_classes =
-  ["class", "tfree", "tvar", "free", "bound", "var", "num", "float", "xnum", "xstr"];
+  ["class", "tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
 
 val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
 
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Thy/latex.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -174,7 +174,7 @@
 fun latex_markup (s, _) =
   if s = Markup.keywordN then ("\\isakeyword{", "}")
   else if s = Markup.commandN then ("\\isacommand{", "}")
-  else ("", "");
+  else Markup.no_output;
 
 fun latex_indent "" _ = ""
   | latex_indent s _ = enclose "\\isaindent{" "}" s;
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -58,9 +58,9 @@
   | T.Ident         => Markup.ident
   | T.LongIdent     => Markup.ident
   | T.SymIdent      => Markup.ident
-  | T.Var           => Markup.ident
-  | T.TypeIdent     => Markup.ident
-  | T.TypeVar       => Markup.ident
+  | T.Var           => Markup.var
+  | T.TypeIdent     => Markup.tfree
+  | T.TypeVar       => Markup.tvar
   | T.Nat           => Markup.ident
   | T.String        => Markup.string
   | T.AltString     => Markup.altstring
diff -r e02b3a32f34f -r dc2663942ccc src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Fri Jan 02 23:36:35 2009 +0100
@@ -1,15 +1,14 @@
 (*  Title:      Pure/Tools/isabelle_process.ML
-    ID:         $Id$
     Author:     Makarius
 
 Isabelle process wrapper -- interaction via external program.
 
 General format of process output:
 
-  (a) unmarked stdout/stderr, no line structure (output should be
+  (1) unmarked stdout/stderr, no line structure (output should be
   processed immediately as it arrives);
 
-  (b) properly marked-up messages, e.g. for writeln channel
+  (2) properly marked-up messages, e.g. for writeln channel
 
   "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
 
@@ -17,13 +16,14 @@
   each, and the remaining text is any number of lines (output is
   supposed to be processed in one piece);
 
-  (c) special init message holds "pid" and "session" property.
+  (3) special init message holds "pid" and "session" property;
+
+  (4) message content is encoded in YXML format.
 *)
 
 signature ISABELLE_PROCESS =
 sig
   val isabelle_processN: string
-  val xmlN: string
   val init: string -> unit
 end;
 
@@ -33,7 +33,6 @@
 (* print modes *)
 
 val isabelle_processN = "isabelle_process";
-val xmlN = "XML";
 
 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
@@ -56,19 +55,14 @@
   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 ts =
-  let
-    val doc = XML.Elem (Markup.messageN, [(Markup.classN, class)], ts);
-    val msg =
-      if print_mode_active xmlN then XML.header ^ XML.string_of doc
-      else YXML.string_of doc;
-  in clean_string [Symbol.STX] msg end;
+fun message_text class body =
+  YXML.element Markup.messageN [(Markup.classN, class)] [clean_string [Symbol.STX] body];
 
-fun message_pos ts = get_first get_pos ts
-and get_pos (elem as XML.Elem (name, atts, ts)) =
-      if name = Markup.positionN then SOME (Position.of_properties atts)
-      else message_pos ts
-  | get_pos _ = NONE;
+fun message_pos trees = trees |> get_first
+  (fn XML.Elem (name, atts, ts) =>
+        if name = Markup.positionN then SOME (Position.of_properties atts)
+        else message_pos ts
+    | _ => NONE);
 
 fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
   (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
@@ -78,19 +72,18 @@
 fun message _ _ _ "" = ()
   | message out_stream ch class body =
       let
-        val (txt, pos) =
-          let val ts = YXML.parse_body body
-          in (message_text class ts, the_default Position.none (message_pos ts)) end;
+        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;
       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 [XML.Text (Session.welcome ())];
+    val text = message_text Markup.initN (Session.welcome ());
   in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
 
 end;