support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions;
Ast.pretty_ast: special treatment of encoded positions;
eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;

--- a/src/Pure/Syntax/ast.ML	Tue Mar 22 11:14:33 2011 +0100
+++ b/src/Pure/Syntax/ast.ML	Tue Mar 22 13:32:20 2011 +0100
@@ -17,7 +17,6 @@
 sig
   include AST0
   val mk_appl: ast -> ast list -> ast
-  val str_of_ast: ast -> string
   val pretty_ast: ast -> Pretty.T
   val pretty_rule: ast * ast -> Pretty.T
   val fold_ast: string -> ast list -> ast
@@ -70,12 +69,11 @@
 
 (** print asts in a LISP-like style **)
 
-fun str_of_ast (Constant a) = quote a
-  | str_of_ast (Variable x) = x
-  | str_of_ast (Appl asts) = "(" ^ (space_implode " " (map str_of_ast asts)) ^ ")";
-
 fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
-  | pretty_ast (Variable x) = Pretty.str x
+  | pretty_ast (Variable x) =
+      (case Lexicon.decode_position x of
+        SOME pos => Lexicon.pretty_position pos
+      | NONE => Pretty.str x)
   | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
 
 fun pretty_rule (lhs, rhs) =
@@ -175,6 +173,9 @@
 val ast_stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
 val ast_stat = Config.bool ast_stat_raw;
 
+fun message head body =
+  Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]);
+
 (*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
 fun normalize ctxt get_rules pre_ast =
   let
@@ -209,8 +210,7 @@
       | rewrite ast = try_headless_rules ast;
 
     fun rewrote old_ast new_ast =
-      if trace then
-        tracing ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast)
+      if trace then tracing (message "rewrote:" (pretty_rule (old_ast, new_ast)))
       else ();
 
     fun norm_root ast =
@@ -239,11 +239,11 @@
       end;
 
 
-    val _ = if trace then tracing ("pre: " ^ str_of_ast pre_ast) else ();
+    val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else ();
     val post_ast = normal pre_ast;
     val _ =
       if trace orelse stat then
-        tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
+        tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^
           string_of_int (! passes) ^ " passes, " ^
           string_of_int (! changes) ^ " changes, " ^
           string_of_int (! failed_matches) ^ " matches failed")

--- a/src/Pure/Syntax/lexicon.ML	Tue Mar 22 11:14:33 2011 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Tue Mar 22 13:32:20 2011 +0100
@@ -42,6 +42,7 @@
     case_fixed: string -> 'a,
     case_default: string -> 'a} -> string -> 'a
   val is_marked: string -> bool
+  val pretty_position: Position.T -> Pretty.T
   val encode_position: Position.T -> string
   val decode_position: string -> Position.T option
 end;
@@ -456,13 +457,20 @@
 
 (* positions *)
 
+val position_dummy = "<position>";
+val position_text = XML.Text position_dummy;
+
+fun pretty_position pos =
+  Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
+
 fun encode_position pos =
-  op ^ (YXML.output_markup (Position.markup pos Markup.position));
+  YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
 
 fun decode_position str =
   (case YXML.parse_body str handle Fail msg => error msg of
-    [XML.Elem ((name, props), [])] =>
-      if name = Markup.positionN then SOME (Position.of_properties props)
+    [XML.Elem ((name, props), [arg])] =>
+      if name = Markup.positionN andalso arg = position_text
+      then SOME (Position.of_properties props)
       else NONE
   | _ => NONE);
 

--- a/src/Pure/Syntax/printer.ML	Tue Mar 22 11:14:33 2011 +0100
+++ b/src/Pure/Syntax/printer.ML	Tue Mar 22 13:32:20 2011 +0100
@@ -415,7 +415,7 @@
       | tokentrT _ _ = NONE
 
     and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
-      | astT (Ast.Variable x, _) = [Pretty.str x]
+      | astT (ast as Ast.Variable x, _) = [Ast.pretty_ast ast]
       | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p)
       | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
       | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);

--- a/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 11:14:33 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 13:32:20 2011 +0100
@@ -55,7 +55,7 @@
   val prop_tr': term -> term
   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
-  val parsetree_to_ast: Proof.context ->
+  val parsetree_to_ast: Proof.context -> bool ->
     (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
   val ast_to_term: Proof.context ->
     (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
@@ -98,32 +98,24 @@
 val constrainAbsC = "_constrainAbs";
 
 fun absfree_proper (x, T, t) =
-  if can Name.dest_internal x then error ("Illegal internal variable in abstraction: " ^ quote x)
+  if can Name.dest_internal x
+  then error ("Illegal internal variable in abstraction: " ^ quote x)
   else Term.absfree (x, T, t);
 
-fun abs_tr (*"_abs"*) [Free (x, T), t] = absfree_proper (x, T, t)
-  | abs_tr (*"_abs"*) [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
-  | abs_tr (*"_abs"*) [Const ("_constrain", _) $ Free (x, T) $ tT, t] =
-      Lexicon.const constrainAbsC $ absfree_proper (x, T, t) $ tT
-  | abs_tr (*"_abs"*) [Const ("_constrain", _) $ Const ("_idtdummy", T) $ tT, t] =
-      Lexicon.const constrainAbsC $ Term.absdummy (T, t) $ tT
-  | abs_tr (*"_abs"*) ts = raise TERM ("abs_tr", ts);
+fun abs_tr [Free (x, T), t] = absfree_proper (x, T, t)
+  | abs_tr [Const ("_idtdummy", T), t] = Term.absdummy (T, t)
+  | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Lexicon.const constrainAbsC $ abs_tr [x, t] $ tT
+  | abs_tr ts = raise TERM ("abs_tr", ts);
 
 
 (* binder *)
 
 fun mk_binder_tr (syn, name) =
   let
-    fun tr (Free (x, T), t) = Lexicon.const name $ absfree_proper (x, T, t)
-      | tr (Const ("_idtdummy", T), t) = Lexicon.const name $ Term.absdummy (T, t)
-      | tr (Const ("_constrain", _) $ Free (x, T) $ tT, t) =
-          Lexicon.const name $ (Lexicon.const constrainAbsC $ absfree_proper (x, T, t) $ tT)
-      | tr (Const ("_constrain", _) $ Const ("_idtdummy", T) $ tT, t) =
-          Lexicon.const name $ (Lexicon.const constrainAbsC $ Term.absdummy (T, t) $ tT)
-      | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
-      | tr (t1, t2) = raise TERM ("binder_tr", [t1, t2]);
-
-    fun binder_tr [idts, body] = tr (idts, body)
+    fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
+      | binder_tr [x, t] =
+          let val abs = abs_tr [x, t] handle TERM _ => raise TERM ("binder_tr", [x, t])
+          in Lexicon.const name $ abs end
       | binder_tr ts = raise TERM ("binder_tr", ts);
   in (syn, binder_tr) end;
 
@@ -533,14 +525,19 @@
 
 (** parsetree_to_ast **)
 
-fun parsetree_to_ast ctxt trf =
+fun parsetree_to_ast ctxt constrain_pos trf =
   let
     fun trans a args =
       (case trf a of
         NONE => Ast.mk_appl (Ast.Constant a) args
       | SOME f => f ctxt args);
 
-    fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
+    fun ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
+          if constrain_pos then
+            Ast.Appl [Ast.Constant "_constrain", ast_of pt,
+              Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
+          else ast_of pt
+      | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
       | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
   in ast_of end;
 

--- a/src/Pure/Syntax/syntax.ML	Tue Mar 22 11:14:33 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Mar 22 13:32:20 2011 +0100
@@ -620,7 +620,7 @@
   (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
     Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
     "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
-    "index", "struct"]);
+    "index", "struct", "id_position", "longid_position"]);
 
 
 
@@ -708,10 +708,10 @@
 
 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
 
-fun read_asts ctxt (Syntax (tabs, _)) xids root (syms, pos) =
+fun read_asts ctxt (Syntax (tabs, _)) raw root (syms, pos) =
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
-    val toks = Lexicon.tokenize lexicon xids syms;
+    val toks = Lexicon.tokenize lexicon raw syms;
     val _ = List.app (Lexicon.report_token ctxt) toks;
 
     val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
@@ -722,7 +722,7 @@
 
     val limit = Config.get ctxt ambiguity_limit;
     fun show_pt pt =
-      Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt (K NONE) pt));
+      Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt false (K NONE) pt));
     val _ =
       if len <= Config.get ctxt ambiguity_level then ()
       else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
@@ -733,7 +733,7 @@
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
             map show_pt (take limit pts))));
   in
-    some_results (Syn_Trans.parsetree_to_ast ctxt (lookup_tr parse_ast_trtab)) pts
+    some_results (Syn_Trans.parsetree_to_ast ctxt false (lookup_tr parse_ast_trtab)) pts
   end;
 
 
@@ -829,11 +829,11 @@
 
 local
 
-fun check_rule (rule as (lhs, rhs)) =
+fun check_rule rule =
   (case Ast.rule_error rule of
     SOME msg =>
       error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
-        Ast.str_of_ast lhs ^ "  ->  " ^ Ast.str_of_ast rhs)
+        Pretty.string_of (Ast.pretty_rule rule))
   | NONE => rule);
 
 fun read_pattern ctxt syn (root, str) =

--- a/src/Pure/Syntax/type_ext.ML	Tue Mar 22 11:14:33 2011 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Tue Mar 22 13:32:20 2011 +0100
@@ -103,15 +103,19 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
+fun is_position (Free (x, _)) = is_some (Lexicon.decode_position x)
+  | is_position _ = false;
+
 fun decode_term get_sort map_const map_free tm =
   let
     val decodeT = typ_of_term (get_sort (term_sorts tm));
 
     fun decode (Const ("_constrain", _) $ t $ typ) =
-          Type.constraint (decodeT typ) (decode t)
-      | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
-          if T = dummyT then Abs (x, decodeT typ, decode t)
-          else Type.constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
+          if is_position typ then decode t
+          else Type.constraint (decodeT typ) (decode t)
+      | decode (Const ("_constrainAbs", _) $ t $ typ) =
+          if is_position typ then decode t
+          else Type.constraint (decodeT typ --> dummyT) (decode t)
       | decode (Abs (x, T, t)) = Abs (x, T, decode t)
       | decode (t $ u) = decode t $ decode u
       | decode (Const (a, T)) =
@@ -162,7 +166,9 @@
 
     fun term_of (Type (a, Ts)) =
           Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
-      | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
+      | term_of (TFree (x, S)) =
+          if is_some (Lexicon.decode_position x) then Lexicon.free x
+          else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
       | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   in term_of ty end;
 

--- a/src/Pure/pure_thy.ML	Tue Mar 22 11:14:33 2011 +0100
+++ b/src/Pure/pure_thy.ML	Tue Mar 22 13:32:20 2011 +0100
@@ -69,9 +69,9 @@
     ("_abs",        typ "'a",                          NoSyn),
     ("",            typ "'a => args",                  Delimfix "_"),
     ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
-    ("",            typ "id => idt",                   Delimfix "_"),
+    ("",            typ "id_position => idt",          Delimfix "_"),
     ("_idtdummy",   typ "idt",                         Delimfix "'_"),
-    ("_idtyp",      typ "id => type => idt",           Mixfix ("_::_", [], 0)),
+    ("_idtyp",      typ "id_position => type => idt",  Mixfix ("_::_", [], 0)),
     ("_idtypdummy", typ "type => idt",                 Mixfix ("'_()::_", [], 0)),
     ("",            typ "idt => idt",                  Delimfix "'(_')"),
     ("",            typ "idt => idts",                 Delimfix "_"),
@@ -80,8 +80,8 @@
     ("",            typ "pttrn => pttrns",             Delimfix "_"),
     ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
     ("",            typ "aprop => aprop",              Delimfix "'(_')"),
-    ("",            typ "id => aprop",                 Delimfix "_"),
-    ("",            typ "longid => aprop",             Delimfix "_"),
+    ("",            typ "id_position => aprop",        Delimfix "_"),
+    ("",            typ "longid_position => aprop",    Delimfix "_"),
     ("",            typ "var => aprop",                Delimfix "_"),
     ("_DDDOT",      typ "aprop",                       Delimfix "..."),
     ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
@@ -91,8 +91,8 @@
     ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
     ("_mk_ofclass", typ "dummy",                       NoSyn),
     ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
-    ("",            typ "id => logic",                 Delimfix "_"),
-    ("",            typ "longid => logic",             Delimfix "_"),
+    ("",            typ "id_position => logic",        Delimfix "_"),
+    ("",            typ "longid_position => logic",    Delimfix "_"),
     ("",            typ "var => logic",                Delimfix "_"),
     ("_DDDOT",      typ "logic",                       Delimfix "..."),
     ("_constify",   typ "num => num_const",            Delimfix "_"),
@@ -104,6 +104,9 @@
     ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     ("_update_name", typ "idt",                        NoSyn),
     (Syntax.constrainAbsC, typ "'a",                   NoSyn),
+    ("_constrain_position", typ "id => id_position",   Delimfix "_"),
+    ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
+    ("_type_constraint_", typ "'a",                    NoSyn),
     (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
     (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
     ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
@@ -116,9 +119,8 @@
     ("_ofsort",           typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
     ("_constrain",        typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
     ("_constrain",        [spropT, typeT] ---> spropT,  Mixfix ("_\\<Colon>_", [4, 0], 3)),
-    ("_idtyp",            typ "id => type => idt",      Mixfix ("_\\<Colon>_", [], 0)),
+    ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
     ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
-    ("_type_constraint_", typ "'a",                     NoSyn),
     ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
     (const "==",          typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
     (const "all_binder",  typ "idts => prop => prop",   Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),