inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
tuned signature;

--- a/NEWS	Sun Jul 10 17:58:11 2011 +0200
+++ b/NEWS	Sun Jul 10 20:59:04 2011 +0200
@@ -146,6 +146,12 @@
 
 *** ML ***
 
+* The inner syntax of sort/type/term/prop supports inlined YXML
+representations within quoted string tokens.  By encoding logical
+entities via Term_XML (in ML or Scala) concrete syntax can be
+bypassed, which is particularly useful for producing bits of text
+under external program control.
+
 * Antiquotations for ML and document preparation are managed as theory
 data, which requires explicit setup.
 

--- a/src/Pure/General/xml_data.ML	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/General/xml_data.ML	Sun Jul 10 20:59:04 2011 +0200
@@ -21,18 +21,18 @@
 
 signature XML_DATA =
 sig
-  structure Make: XML_DATA_OPS where type 'a T = 'a -> XML.body
+  structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body
   exception XML_ATOM of string
   exception XML_BODY of XML.body
-  structure Dest: XML_DATA_OPS where type 'a T = XML.body -> 'a
+  structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a
 end;
 
 structure XML_Data: XML_DATA =
 struct
 
-(** make **)
+(** encode **)
 
-structure Make =
+structure Encode =
 struct
 
 type 'a T = 'a -> XML.body;
@@ -83,12 +83,12 @@
 
 
 
-(** dest **)
+(** decode **)
 
 exception XML_ATOM of string;
 exception XML_BODY of XML.tree list;
 
-structure Dest =
+structure Decode =
 struct
 
 type 'a T = XML.body -> 'a;

--- a/src/Pure/General/xml_data.scala	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/General/xml_data.scala	Sun Jul 10 20:59:04 2011 +0200
@@ -10,9 +10,9 @@
 
 object XML_Data
 {
-  /** make **/
+  /** encode **/
 
-  object Make
+  object Encode
   {
     type T[A] = A => XML.Body
 
@@ -76,12 +76,12 @@
 
 
 
-  /** dest **/
+  /** decode **/
 
   class XML_Atom(s: String) extends Exception(s)
   class XML_Body(body: XML.Body) extends Exception
 
-  object Dest
+  object Decode
   {
     type T[A] = XML.Body => A
 

--- a/src/Pure/General/yxml.ML	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/General/yxml.ML	Sun Jul 10 20:59:04 2011 +0200
@@ -16,6 +16,7 @@
 signature YXML =
 sig
   val escape_controls: string -> string
+  val detect: string -> bool
   val output_markup: Markup.T -> string * string
   val element: string -> XML.attributes -> string list -> string
   val string_of_body: XML.body -> string
@@ -49,6 +50,8 @@
 val XY = X ^ Y;
 val XYX = XY ^ X;
 
+val detect = exists_string (fn s => s = X);
+
 
 (* output *)
 

--- a/src/Pure/Isar/token.ML	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/Isar/token.ML	Sun Jul 10 20:59:04 2011 +0200
@@ -180,8 +180,9 @@
 
 (* token content *)
 
-fun source_of (Token ((source, (pos, _)), _, _)) =
-  YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
+fun source_of (Token ((source, (pos, _)), (_, x), _)) =
+  if YXML.detect x then x
+  else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
 
 fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
 

--- a/src/Pure/PIDE/isar_document.ML	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 20:59:04 2011 +0200
@@ -18,10 +18,10 @@
         val old_id = Document.parse_id old_id_string;
         val new_id = Document.parse_id new_id_string;
         val edits = YXML.parse_body edits_yxml |>
-          let open XML_Data.Dest
+          let open XML_Data.Decode
           in list (pair string (option (list (pair (option int) (option int))))) end;
         val headers = YXML.parse_body headers_yxml |>
-          let open XML_Data.Dest
+          let open XML_Data.Decode
           in list (pair string (triple string (list string) (list string))) end;
 
       val await_cancellation = Document.cancel_execution state;

--- a/src/Pure/PIDE/isar_document.scala	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 20:59:04 2011 +0200
@@ -143,12 +143,12 @@
       edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
   {
     val arg1 =
-    { import XML_Data.Make._
+    { import XML_Data.Encode._
       list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
 
     val arg2 =
-    { import XML_Data.Make._
-      list(pair(string, Thy_Header.make_xml_data))(headers) }
+    { import XML_Data.Encode._
+      list(pair(string, Thy_Header.encode_xml_data))(headers) }
 
     input("Isar_Document.edit_version",
       Document.ID(old_id), Document.ID(new_id),

--- a/src/Pure/Syntax/syntax.ML	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Jul 10 20:59:04 2011 +0200
@@ -17,7 +17,8 @@
   val ambiguity_level: int Config.T
   val ambiguity_limit: int Config.T
   val read_token: string -> Symbol_Pos.T list * Position.T
-  val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T
+  val parse_token: Proof.context -> (XML.tree list -> 'a) ->
+    Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   val parse_sort: Proof.context -> string -> sort
   val parse_typ: Proof.context -> string -> typ
   val parse_term: Proof.context -> string -> term
@@ -193,11 +194,10 @@
   Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
 
 
-(* read token -- with optional YXML encoding of position *)
+(* outer syntax token -- with optional YXML content *)
 
-fun read_token str =
+fun explode_token tree =
   let
-    val tree = YXML.parse str handle Fail msg => error msg;
     val text = XML.content_of [tree];
     val pos =
       (case tree of
@@ -207,15 +207,26 @@
       | XML.Text _ => Position.none);
   in (Symbol_Pos.explode (text, pos), pos) end;
 
+fun read_token str = explode_token (YXML.parse str handle Fail msg => error msg);
+
+fun parse_token ctxt decode markup parse str =
+  let
+    fun parse_tree tree =
+      let
+        val (syms, pos) = explode_token tree;
+        val _ = Context_Position.report ctxt pos markup;
+      in parse (syms, pos) end;
+  in
+    (case YXML.parse_body str handle Fail msg => error msg of
+      body as [tree as XML.Elem ((name, _), _)] =>
+        if name = Markup.tokenN then parse_tree tree else decode body
+    | [tree as XML.Text _] => parse_tree tree
+    | body => decode body)
+  end;
+
 
 (* (un)parsing *)
 
-fun parse_token ctxt markup str =
-  let
-    val (syms, pos) = read_token str;
-    val _ = Context_Position.report ctxt pos markup;
-  in (syms, pos) end;
-
 val parse_sort = operation #parse_sort;
 val parse_typ = operation #parse_typ;
 val parse_term = operation #parse_term;

--- a/src/Pure/Syntax/syntax_phases.ML	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Jul 10 20:59:04 2011 +0200
@@ -320,80 +320,79 @@
   cat_error msg ("Failed to parse " ^ kind ^
     Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
 
-fun parse_sort ctxt text =
-  let
-    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
-    val S =
+fun parse_sort ctxt =
+  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
+    (fn (syms, pos) =>
       parse_raw ctxt "sort" (syms, pos)
       |> report_result ctxt pos
       |> sort_of_term
-      handle ERROR msg => parse_failed ctxt pos msg "sort";
-  in Type.minimize_sort (Proof_Context.tsig_of ctxt) S end;
+      |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
+      handle ERROR msg => parse_failed ctxt pos msg "sort");
 
-fun parse_typ ctxt text =
-  let
-    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
-    val T =
+fun parse_typ ctxt =
+  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
+    (fn (syms, pos) =>
       parse_raw ctxt "type" (syms, pos)
       |> report_result ctxt pos
       |> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) t)
-      handle ERROR msg => parse_failed ctxt pos msg "type";
-  in T end;
+      handle ERROR msg => parse_failed ctxt pos msg "type");
 
-fun parse_term is_prop ctxt text =
+fun parse_term is_prop ctxt =
   let
     val (markup, kind, root, constrain) =
       if is_prop
       then (Markup.prop, "proposition", "prop", Type.constraint propT)
       else (Markup.term, "term", Config.get ctxt Syntax.root, I);
-    val (syms, pos) = Syntax.parse_token ctxt markup text;
+    val decode = constrain o Term_XML.Decode.term;
   in
-    let
-      val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
-      val ambiguity = length (proper_results results);
-
-      val level = Config.get ctxt Syntax.ambiguity_level;
-      val limit = Config.get ctxt Syntax.ambiguity_limit;
+    Syntax.parse_token ctxt decode markup
+      (fn (syms, pos) =>
+        let
+          val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
+          val ambiguity = length (proper_results results);
 
-      val ambig_msg =
-        if ambiguity > 1 andalso ambiguity <= level then
-          ["Got more than one parse tree.\n\
-          \Retry with smaller syntax_ambiguity_level for more information."]
-        else [];
+          val level = Config.get ctxt Syntax.ambiguity_level;
+          val limit = Config.get ctxt Syntax.ambiguity_limit;
 
-      (*brute-force disambiguation via type-inference*)
-      fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
-        handle exn as ERROR _ => Exn.Exn exn;
+          val ambig_msg =
+            if ambiguity > 1 andalso ambiguity <= level then
+              ["Got more than one parse tree.\n\
+              \Retry with smaller syntax_ambiguity_level for more information."]
+            else [];
+
+          (*brute-force disambiguation via type-inference*)
+          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
+            handle exn as ERROR _ => Exn.Exn exn;
 
-      val results' =
-        if ambiguity > 1 then
-          (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
-            check results
-        else results;
-      val reports' = fst (hd results');
+          val results' =
+            if ambiguity > 1 then
+              (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
+                check results
+            else results;
+          val reports' = fst (hd results');
 
-      val errs = map snd (failed_results results');
-      val checked = map snd (proper_results results');
-      val len = length checked;
+          val errs = map snd (failed_results results');
+          val checked = map snd (proper_results results');
+          val len = length checked;
 
-      val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
-    in
-      if len = 0 then
-        report_result ctxt pos
-          [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
-      else if len = 1 then
-        (if ambiguity > level then
-          Context_Position.if_visible ctxt warning
-            "Fortunately, only one parse tree is type correct.\n\
-            \You may still want to disambiguate your grammar or your input."
-        else (); report_result ctxt pos results')
-      else
-        report_result ctxt pos
-          [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
-            (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
-              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-              map show_term (take limit checked))))))]
-    end handle ERROR msg => parse_failed ctxt pos msg kind
+          val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
+        in
+          if len = 0 then
+            report_result ctxt pos
+              [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
+          else if len = 1 then
+            (if ambiguity > level then
+              Context_Position.if_visible ctxt warning
+                "Fortunately, only one parse tree is type correct.\n\
+                \You may still want to disambiguate your grammar or your input."
+            else (); report_result ctxt pos results')
+          else
+            report_result ctxt pos
+              [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
+                (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
+                  (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
+                  map show_term (take limit checked))))))]
+        end handle ERROR msg => parse_failed ctxt pos msg kind)
   end;
 
 

--- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 20:59:04 2011 +0200
@@ -31,10 +31,10 @@
       Header(f(name), imports.map(f), uses.map(f))
   }
 
-  val make_xml_data: XML_Data.Make.T[Header] =
+  val encode_xml_data: XML_Data.Encode.T[Header] =
   {
     case Header(name, imports, uses) =>
-      import XML_Data.Make._
+      import XML_Data.Encode._
       triple(string, list(string), list(string))(name, imports, uses)
   }
 

--- a/src/Pure/Tools/find_theorems.ML	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sun Jul 10 20:59:04 2011 +0200
@@ -139,8 +139,8 @@
           |> (if rem_dups then cons ("rem_dups", "") else I)
           |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
       in
-        XML.Elem (("Query", properties), XML_Data.Make.list
-          (XML_Data.Make.pair XML_Data.Make.bool (single o xml_of_criterion)) criteria)
+        XML.Elem (("Query", properties), XML_Data.Encode.list
+          (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
       end
   | xml_of_query _ = raise Fail "cannot serialize goal";
 
@@ -149,7 +149,7 @@
         val rem_dups = Properties.defined properties "rem_dups";
         val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
         val criteria =
-          XML_Data.Dest.list (XML_Data.Dest.pair XML_Data.Dest.bool 
+          XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
             (criterion_of_xml o the_single)) body;
       in
         {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
@@ -190,12 +190,12 @@
     val properties =
       if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
   in
-    XML.Elem (("Result", properties), XML_Data.Make.list (single o xml_of_theorem) theorems)
+    XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
   end;
 
 fun result_of_xml (XML.Elem (("Result", properties), body)) =
       (Properties.get properties "found" |> Option.map Markup.parse_int,
-       XML_Data.Dest.list (theorem_of_xml o the_single) body)
+       XML_Data.Decode.list (theorem_of_xml o the_single) body)
   | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
 
 fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm

--- a/src/Pure/term.scala	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/term.scala	Sun Jul 10 20:59:04 2011 +0200
@@ -31,58 +31,61 @@
   case class Bound(index: Int) extends Term
   case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
   case class App(fun: Term, arg: Term) extends Term
+}
+
+
+object Term_XML
+{
+  import Term._
 
 
   /* XML data representation */
 
-  object XML
+  object Encode
   {
-    object Make
-    {
-      import XML_Data.Make._
+    import XML_Data.Encode._
 
-      val indexname: T[Indexname] = pair(string, int)
+    val indexname: T[Indexname] = pair(string, int)
 
-      val sort: T[Sort] = list(string)
+    val sort: T[Sort] = list(string)
 
-      def typ: T[Typ] =
-        variant[Typ](List(
-          { case Type(a, b) => pair(string, list(typ))((a, b)) },
-          { case TFree(a, b) => pair(string, sort)((a, b)) },
-          { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
+    def typ: T[Typ] =
+      variant[Typ](List(
+        { case Type(a, b) => pair(string, list(typ))((a, b)) },
+        { case TFree(a, b) => pair(string, sort)((a, b)) },
+        { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
 
-      def term: T[Term] =
-        variant[Term](List(
-          { case Const(a, b) => pair(string, typ)((a, b)) },
-          { case Free(a, b) => pair(string, typ)((a, b)) },
-          { case Var(a, b) => pair(indexname, typ)((a, b)) },
-          { case Bound(a) => int(a) },
-          { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
-          { case App(a, b) => pair(term, term)((a, b)) }))
-    }
+    def term: T[Term] =
+      variant[Term](List(
+        { case Const(a, b) => pair(string, typ)((a, b)) },
+        { case Free(a, b) => pair(string, typ)((a, b)) },
+        { case Var(a, b) => pair(indexname, typ)((a, b)) },
+        { case Bound(a) => int(a) },
+        { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
+        { case App(a, b) => pair(term, term)((a, b)) }))
+  }
 
-    object Dest
-    {
-      import XML_Data.Dest._
+  object Decode
+  {
+    import XML_Data.Decode._
 
-      val indexname: T[Indexname] = pair(string, int)
+    val indexname: T[Indexname] = pair(string, int)
 
-      val sort: T[Sort] = list(string)
+    val sort: T[Sort] = list(string)
 
-      def typ: T[Typ] =
-        variant[Typ](List(
-          (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
-          (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
-          (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
+    def typ: T[Typ] =
+      variant[Typ](List(
+        (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
+        (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
+        (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
 
-      def term: T[Term] =
-        variant[Term](List(
-          (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
-          (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
-          (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
-          (x => Bound(int(x))),
-          (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
-          (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
-    }
+    def term: T[Term] =
+      variant[Term](List(
+        (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
+        (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
+        (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
+        (x => Bound(int(x))),
+        (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
+        (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
   }
 }

--- a/src/Pure/term_xml.ML	Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/term_xml.ML	Sun Jul 10 20:59:04 2011 +0200
@@ -15,19 +15,19 @@
 
 signature TERM_XML =
 sig
-  structure Make: TERM_XML_OPS where type 'a T = 'a XML_Data.Make.T
-  structure Dest: TERM_XML_OPS where type 'a T = 'a XML_Data.Dest.T
+  structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
+  structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
 end;
 
 structure Term_XML: TERM_XML =
 struct
 
-(* make *)
+(* encode *)
 
-structure Make =
+structure Encode =
 struct
 
-open XML_Data.Make;
+open XML_Data.Encode;
 
 val indexname = pair string int;
 
@@ -49,12 +49,12 @@
 end;
 
 
-(* dest *)
+(* decode *)
 
-structure Dest =
+structure Decode =
 struct
 
-open XML_Data.Dest;
+open XML_Data.Decode;
 
 val indexname = pair string int;