# HG changeset patch
# User wenzelm
# Date 1394195350 -3600
# Node ID 43815ee659bc8c7b3819f398699f1ab179bbe576
# Parent  9962ca0875c98313c0d557e76aa62f8a3cc03390
more basic const report (without completion) for known Const within syntax tree, which usually refers to special syntax (without proper @{const_syntax} markers);
tuned;

diff -r 9962ca0875c9 -r 43815ee659bc src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Mar 07 11:48:11 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Mar 07 13:29:10 2014 +0100
@@ -228,6 +228,22 @@
       Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
   in (c', reports) end;
 
+local
+
+fun get_free ctxt x =
+  let
+    val fixed = Variable.lookup_fixed ctxt x;
+    val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
+    val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
+  in
+    if Variable.is_const ctxt x then NONE
+    else if is_some fixed then fixed
+    else if not is_const orelse is_declared then SOME x
+    else NONE
+  end;
+
+in
+
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Res tm) =
       let
@@ -235,24 +251,6 @@
         fun report ps = Position.store_reports reports ps;
         val append_reports = Position.append_reports reports;
 
-        fun get_free x =
-          let
-            val fixed = Variable.lookup_fixed ctxt x;
-            val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
-            val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
-          in
-            if Variable.is_const ctxt x then NONE
-            else if is_some fixed then fixed
-            else if not is_const orelse is_declared then SOME x
-            else NONE
-          end;
-
-        fun the_const (a, ps) =
-          let
-            val (c, rs) = decode_const ctxt (a, ps);
-            val _ = append_reports rs;
-          in c end;
-
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
                 SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
@@ -274,15 +272,20 @@
                   let
                     val c =
                       (case try Lexicon.unmark_const a of
-                        SOME c => (report ps (markup_const ctxt) c; c)
-                      | NONE => the_const (a, ps));
+                        SOME c => c
+                      | NONE => #1 (decode_const ctxt (a, [])));
+                    val _ = report ps (markup_const ctxt) c;
                   in Const (c, T) end)
           | decode ps _ _ (Free (a, T)) =
               ((Name.reject_internal (a, ps) handle ERROR msg =>
                   error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
-                (case get_free a of
+                (case get_free ctxt a of
                   SOME x => (report ps (markup_free ctxt) x; Free (x, T))
-                | NONE => Const (the_const (a, ps), T)))
+                | NONE =>
+                    let
+                      val (c, rs) = decode_const ctxt (a, ps);
+                      val _ = append_reports rs;
+                    in Const (c, T) end))
           | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
           | decode ps _ bs (t as Bound i) =
               (case try (nth bs) i of
@@ -292,6 +295,8 @@
         val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
       in (! reports, tm') end;
 
+end;
+
 
 
 (** parse **)