merged

--- a/src/HOL/Num.thy	Mon May 27 20:09:20 2013 +0200
+++ b/src/HOL/Num.thy	Mon May 27 22:26:08 2013 +0200
@@ -326,14 +326,15 @@
     fun num_tr' sign ctxt T [n] =
       let
         val k = dest_num n;
-        val t' = Syntax.const @{syntax_const "_Numeral"} $
-          Syntax.free (sign ^ string_of_int k);
+        val t' =
+          Syntax.const @{syntax_const "_Numeral"} $
+            Syntax.free (sign ^ string_of_int k);
       in
         (case T of
           Type (@{type_name fun}, [_, T']) =>
             if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
             else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
-        | T' => if T' = dummyT then t' else raise Match)
+        | _ => if T = dummyT then t' else raise Match)
       end;
   in
    [(@{const_syntax numeral}, num_tr' ""),

--- a/src/Pure/Syntax/lexicon.ML	Mon May 27 20:09:20 2013 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon May 27 22:26:08 2013 +0200
@@ -169,7 +169,9 @@
 (* markup *)
 
 fun literal_markup s =
-  if Symbol.is_ascii_identifier s then Markup.literal else Markup.delimiter;
+  if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s)
+  then Markup.literal
+  else Markup.delimiter;
 
 val token_kind_markup =
  fn TFreeSy => Markup.tfree

--- a/src/Pure/Syntax/printer.ML	Mon May 27 20:09:20 2013 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon May 27 22:26:08 2013 +0200
@@ -10,7 +10,6 @@
   val show_types: bool Config.T
   val show_sorts: bool Config.T
   val show_free_types: bool Config.T
-  val show_all_types: bool Config.T
   val show_markup: bool Config.T
   val show_structs: bool Config.T
   val show_question_marks: bool Config.T
@@ -60,7 +59,6 @@
 val show_sorts = Config.bool show_sorts_raw;
 
 val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
-val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
 
 val show_markup_default = Unsynchronized.ref false;
 val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));

--- a/src/Pure/Syntax/syntax_phases.ML	Mon May 27 20:09:20 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon May 27 22:26:08 2013 +0200
@@ -136,7 +136,7 @@
 
 (* parsetree_to_ast *)
 
-fun parsetree_to_ast ctxt raw trf parsetree =
+fun parsetree_to_ast ctxt trf parsetree =
   let
     val reports = Unsynchronized.ref ([]: Position.report list);
     fun report pos = Position.store_reports reports [pos];
@@ -155,12 +155,10 @@
       Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok));
 
     fun ast_of_dummy a tok =
-      if raw then Ast.Constant a
-      else Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
+      Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
 
     fun asts_of_position c tok =
-      if raw then asts_of_token tok
-      else [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
+      [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
 
     and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
           let
@@ -322,7 +320,7 @@
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
             map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))];
 
-  in (ambig_msgs, map (parsetree_to_ast ctxt raw ast_tr) pts) end;
+  in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;
 
 fun parse_tree ctxt root input =
   let
@@ -421,19 +419,32 @@
   let
     val syn = Proof_Context.syn_of ctxt;
 
-    fun constify (ast as Ast.Constant _) = ast
-      | constify (ast as Ast.Variable x) =
+    val reports = Unsynchronized.ref ([]: Position.report list);
+    fun report ps = Position.store_reports reports ps;
+
+    fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c);
+    fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x);
+    fun decode_appl ps asts = Ast.Appl (map (decode ps) asts)
+    and decode ps (Ast.Constant c) = decode_const ps c
+      | decode ps (Ast.Variable x) =
           if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
-          then Ast.Constant x
-          else ast
-      | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
+          then decode_const ps x
+          else decode_var ps x
+      | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) =
+          if member (op =) Term_Position.markers c then
+            (case Term_Position.decode x of
+              SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args)
+            | NONE => decode_appl ps asts)
+          else decode_appl ps asts
+      | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
     val (syms, pos) = Syntax.read_token str;
-  in
-    parse_asts ctxt true root (syms, pos)
-    |> uncurry (report_result ctxt pos)
-    |> constify
-  end;
+    val ast =
+      parse_asts ctxt true root (syms, pos)
+      |> uncurry (report_result ctxt pos)
+      |> decode [];
+    val _ = Context_Position.reports ctxt (! reports);
+  in ast end;
 
 
 
@@ -541,48 +552,43 @@
             (mark Ts t1 $ mark Ts t2);
   in mark [] tm end;
 
-in
-
-fun term_to_ast idents is_syntax_const ctxt trf tm =
+fun prune_types ctxt tm =
   let
-    val show_types =
-      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
-      Config.get ctxt show_all_types;
-    val show_structs = Config.get ctxt show_structs;
     val show_free_types = Config.get ctxt show_free_types;
-    val show_all_types = Config.get ctxt show_all_types;
-    val show_markup = Config.get ctxt show_markup;
 
-    val {structs, fixes} = idents;
-
-    fun prune_typs (t_seen as (Const _, _)) = t_seen
-      | prune_typs (t as Free (x, ty), seen) =
+    fun prune (t_seen as (Const _, _)) = t_seen
+      | prune (t as Free (x, ty), seen) =
           if ty = dummyT then (t, seen)
           else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
           else (t, t :: seen)
-      | prune_typs (t as Var (xi, ty), seen) =
+      | prune (t as Var (xi, ty), seen) =
           if ty = dummyT then (t, seen)
           else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
           else (t, t :: seen)
-      | prune_typs (t_seen as (Bound _, _)) = t_seen
-      | prune_typs (Abs (x, ty, t), seen) =
-          let val (t', seen') = prune_typs (t, seen);
+      | prune (t_seen as (Bound _, _)) = t_seen
+      | prune (Abs (x, ty, t), seen) =
+          let val (t', seen') = prune (t, seen);
           in (Abs (x, ty, t'), seen') end
-      | prune_typs (t1 $ t2, seen) =
+      | prune (t1 $ t2, seen) =
           let
-            val (t1', seen') = prune_typs (t1, seen);
-            val (t2', seen'') = prune_typs (t2, seen');
+            val (t1', seen') = prune (t1, seen);
+            val (t2', seen'') = prune (t2, seen');
           in (t1' $ t2', seen'') end;
+  in #1 (prune (tm, [])) end;
 
-    fun mark_atoms ((t as Const (c, _)) $ u) =
+fun mark_atoms {structs, fixes} is_syntax_const ctxt tm =
+  let
+    val show_structs = Config.get ctxt show_structs;
+
+    fun mark ((t as Const (c, _)) $ u) =
           if member (op =) Pure_Thy.token_markers c
-          then t $ u else mark_atoms t $ mark_atoms u
-      | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
-      | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
-      | mark_atoms (t as Const (c, T)) =
+          then t $ u else mark t $ mark u
+      | mark (t $ u) = mark t $ mark u
+      | mark (Abs (x, T, t)) = Abs (x, T, mark t)
+      | mark (t as Const (c, T)) =
           if is_syntax_const c then t
           else Const (Lexicon.mark_const c, T)
-      | mark_atoms (t as Free (x, T)) =
+      | mark (t as Free (x, T)) =
           let val i = find_index (fn s => s = x) structs + 1 in
             if i = 0 andalso member (op =) fixes x then
               Const (Lexicon.mark_fixed x, T)
@@ -590,10 +596,18 @@
               Syntax.const "_struct" $ Syntax.const "_indexdefault"
             else Syntax.const "_free" $ t
           end
-      | mark_atoms (t as Var (xi, T)) =
+      | mark (t as Var (xi, T)) =
           if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
           else Syntax.const "_var" $ t
-      | mark_atoms a = a;
+      | mark a = a;
+  in mark tm end;
+
+in
+
+fun term_to_ast idents is_syntax_const ctxt trf tm =
+  let
+    val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
+    val show_markup = Config.get ctxt show_markup;
 
     fun ast_of tm =
       (case strip_comb tm of
@@ -610,10 +624,7 @@
           in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
       | (Const ("_idtdummy", T), ts) =>
           Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
-      | (const as Const (c, T), ts) =>
-          if show_all_types
-          then Ast.mk_appl (constrain const T) (map ast_of ts)
-          else trans c T ts
+      | (const as Const (c, T), ts) => trans c T ts
       | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
 
     and trans a T args = ast_of (trf a ctxt T args)
@@ -627,8 +638,8 @@
   in
     tm
     |> mark_aprop
-    |> show_types ? (#1 o prune_typs o rpair [])
-    |> mark_atoms
+    |> show_types ? prune_types ctxt
+    |> mark_atoms idents is_syntax_const ctxt
     |> ast_of
   end;
 
@@ -666,9 +677,7 @@
   let
     val show_markup = Config.get ctxt show_markup;
     val show_sorts = Config.get ctxt show_sorts;
-    val show_types =
-      Config.get ctxt show_types orelse show_sorts orelse
-      Config.get ctxt show_all_types;
+    val show_types = Config.get ctxt show_types orelse show_sorts;
 
     val syn = Proof_Context.syn_of ctxt;
     val prtabs = Syntax.prtabs syn;

--- a/src/Pure/goal_display.ML	Mon May 27 20:09:20 2013 +0200
+++ b/src/Pure/goal_display.ML	Mon May 27 22:26:08 2013 +0200
@@ -71,10 +71,7 @@
   let
     val ctxt = ctxt0
       |> Config.put show_free_types false
-      |> Config.put show_types
-       (Config.get ctxt0 show_types orelse
-        Config.get ctxt0 show_sorts orelse
-        Config.get ctxt0 show_all_types)
+      |> Config.put show_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts)
       |> Config.put show_sorts false;
 
     val show_sorts0 = Config.get ctxt0 show_sorts;