thm_antiq: produce error at runtime, not compile time;
authorwenzelm
Thu Mar 20 17:38:55 2008 +0100 (2008-03-20 ago)
changeset 263683e74b09ce466
parent 26367 06635166d211
child 26369 01ee1168088b
thm_antiq: produce error at runtime, not compile time;
tuned;
src/Pure/ML/ml_context.ML
     1.1 --- a/src/Pure/ML/ml_context.ML	Thu Mar 20 17:38:54 2008 +0100
     1.2 +++ b/src/Pure/ML/ml_context.ML	Thu Mar 20 17:38:55 2008 +0100
     1.3 @@ -275,20 +275,25 @@
     1.4    | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i
     1.5    | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
     1.6  
     1.7 -fun thm_sel name_pos =
     1.8 -  Scan.option Args.thm_sel >> (fn sel => "Facts.Named " ^
     1.9 +fun print_named args =
    1.10 +  "Facts.Named " ^
    1.11      ML_Syntax.print_pair (ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position)
    1.12 -      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name_pos, sel));
    1.13 +      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) args;
    1.14  
    1.15 -fun thm_antiq kind get = value_antiq kind
    1.16 -  (Scan.lift (Args.position Args.name :-- thm_sel) >> (fn ((name, _), sel) =>
    1.17 -    (name, get ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel)));
    1.18 +fun thm_antiq kind get get_name = value_antiq kind
    1.19 +  ((Scan.state >> Context.proof_of) --
    1.20 +    Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel)
    1.21 +  >> (fn (ctxt, thmspec as ((name, _), _)) =>
    1.22 +      let
    1.23 +        val _ = get ctxt (Facts.Named thmspec);
    1.24 +        val thmspec_txt = ML_Syntax.atomic (print_named thmspec);
    1.25 +      in (name, get_name ^ " (ML_Context.the_local_context ()) " ^ thmspec_txt) end));
    1.26  
    1.27  in
    1.28  
    1.29  val _ = add_keywords ["(", ")", "-", ","];
    1.30 -val _ = thm_antiq "thm" "ProofContext.get_fact_single";
    1.31 -val _ = thm_antiq "thms" "ProofContext.get_fact";
    1.32 +val _ = thm_antiq "thm" ProofContext.get_fact_single "ProofContext.get_fact_single";
    1.33 +val _ = thm_antiq "thms" ProofContext.get_fact "ProofContext.get_fact";
    1.34  
    1.35  end;
    1.36