# HG changeset patch
# User wenzelm
# Date 1267300311 -3600
# Node ID 3881972fcfca841f8e45bfed22afe86c15d9bf9b
# Parent  aec00d4ec03d4d5a1d3630ce749dcd9493f9b0d6
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;

diff -r aec00d4ec03d -r 3881972fcfca src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat Feb 27 13:55:03 2010 +0100
+++ b/src/Pure/Isar/args.ML	Sat Feb 27 20:51:51 2010 +0100
@@ -55,8 +55,8 @@
   val term_abbrev: term context_parser
   val prop: term context_parser
   val type_name: bool -> string context_parser
-  val const: string context_parser
-  val const_proper: string context_parser
+  val const: bool -> string context_parser
+  val const_proper: bool -> string context_parser
   val bang_facts: thm list context_parser
   val goal_spec: ((int -> tactic) -> tactic) context_parser
   val parse: token list parser
@@ -213,10 +213,12 @@
   Scan.peek (fn ctxt => named_typ (ProofContext.read_type_name (Context.proof_of ctxt) strict))
   >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
 
-val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of)
+fun const strict =
+  Scan.peek (fn ctxt => named_term (ProofContext.read_const (Context.proof_of ctxt) strict))
   >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
 
-val const_proper = Scan.peek (named_term o ProofContext.read_const_proper o Context.proof_of)
+fun const_proper strict =
+  Scan.peek (fn ctxt => named_term (ProofContext.read_const_proper (Context.proof_of ctxt) strict))
   >> (fn Const (c, _) => c | _ => "");
 
 
diff -r aec00d4ec03d -r 3881972fcfca src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Feb 27 13:55:03 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Feb 27 20:51:51 2010 +0100
@@ -53,8 +53,8 @@
   val inferred_param: string -> Proof.context -> typ * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
   val read_type_name: Proof.context -> bool -> string -> typ
-  val read_const_proper: Proof.context -> string -> term
-  val read_const: Proof.context -> string -> term
+  val read_const_proper: Proof.context -> bool -> string -> term
+  val read_const: Proof.context -> bool -> string -> term
   val allow_dummies: Proof.context -> Proof.context
   val decode_term: Proof.context -> term -> term
   val standard_infer_types: Proof.context -> term list -> term list
@@ -360,7 +360,7 @@
           (Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
   | NONE => Pretty.mark Markup.var (Pretty.str s));
 
-fun class_markup _ c =    (* FIXME authentic name *)
+fun class_markup _ c =    (* FIXME authentic syntax *)
   Pretty.mark (Markup.tclassN, []) (Pretty.str c);
 
 fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
@@ -405,19 +405,27 @@
 
 val token_content = Syntax.read_token #>> Symbol_Pos.content;
 
-fun prep_const_proper ctxt (c, pos) =
-  let val t as (Const (d, _)) =
-    (case Variable.lookup_const ctxt c of
-      SOME d => Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => error msg)
-    | NONE => Consts.read_const (consts_of ctxt) c)
-  in Position.report (Markup.const d) pos; t end;
+fun prep_const_proper ctxt strict (c, pos) =
+  let
+    fun err msg = error (msg ^ Position.str_of pos);
+    val consts = consts_of ctxt;
+    val t as Const (d, _) =
+      (case Variable.lookup_const ctxt c of
+        SOME d =>
+          Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg)
+      | NONE => Consts.read_const consts c);
+    val _ =
+      if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
+      else ();
+    val _ = Position.report (Markup.const d) pos;
+  in t end;
 
 in
 
-fun read_type_name ctxt strict str =
+fun read_type_name ctxt strict text =
   let
     val thy = theory_of ctxt;
-    val (c, pos) = token_content str;
+    val (c, pos) = token_content text;
   in
     if Syntax.is_tid c then
      (Position.report Markup.tfree pos;
@@ -436,16 +444,16 @@
       in Type (d, replicate args dummyT) end
   end;
 
-fun read_const_proper ctxt = prep_const_proper ctxt o token_content;
+fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
 
-fun read_const ctxt str =
-  let val (c, pos) = token_content str in
+fun read_const ctxt strict text =
+  let val (c, pos) = token_content text in
     (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
         (Position.report (Markup.name x
             (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
           Free (x, infer_type ctxt x))
-    | _ => prep_const_proper ctxt (c, pos))
+    | _ => prep_const_proper ctxt strict (c, pos))
   end;
 
 end;
@@ -574,7 +582,7 @@
   let
     val _ = no_skolem false x;
     val sko = lookup_skolem ctxt x;
-    val is_const = can (read_const_proper ctxt) x orelse Long_Name.is_qualified x;
+    val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
     val is_declared = is_some (def_type (x, ~1));
   in
     if Variable.is_const ctxt x then NONE
@@ -588,7 +596,7 @@
 fun term_context ctxt =
   let val thy = theory_of ctxt in
    {get_sort = get_sort thy (Variable.def_sort ctxt),
-    map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt a)))
+    map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
       handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
     map_free = intern_skolem ctxt (Variable.def_type ctxt false),
     map_type = Sign.intern_tycons thy,
@@ -994,7 +1002,7 @@
 
 fun const_ast_tr intern ctxt [Syntax.Variable c] =
       let
-        val Const (c', _) = read_const_proper ctxt c;
+        val Const (c', _) = read_const_proper ctxt false c;
         val d = if intern then Syntax.mark_const c' else c;
       in Syntax.Constant d end
   | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
diff -r aec00d4ec03d -r 3881972fcfca src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Feb 27 13:55:03 2010 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Feb 27 20:51:51 2010 +0100
@@ -259,7 +259,7 @@
   lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
 
 val notation = gen_notation (K I);
-val notation_cmd = gen_notation ProofContext.read_const;
+val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false);
 
 
 (* fact statements *)
diff -r aec00d4ec03d -r 3881972fcfca src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Feb 27 13:55:03 2010 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Feb 27 20:51:51 2010 +0100
@@ -528,7 +528,7 @@
 val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style;
 val _ = basic_entity "term_type" (Term_Style.parse -- Args.term) pretty_term_typ;
 val _ = basic_entity "typeof" (Term_Style.parse -- Args.term) pretty_term_typeof;
-val _ = basic_entity "const" Args.const_proper pretty_const;
+val _ = basic_entity "const" (Args.const_proper false) pretty_const;
 val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
 val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
 val _ = basic_entity "text" (Scan.lift Args.name) (K pretty_text);