# HG changeset patch
# User ballarin
# Date 1227546228 -3600
# Node ID db2816a37a346b842d66a3cca6482def04c7f9ed
# Parent  141ed00656aefcb7a969ac009640ab658b18fdc3
Read/cert_statement for theorem statements.

diff -r 141ed00656ae -r db2816a37a34 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Nov 24 18:02:52 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Nov 24 18:03:48 2008 +0100
@@ -15,6 +15,12 @@
   type expression = (string * string map) expr * (Name.binding * string option * mixfix) list
 (*  type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list *)
 
+  (* Processing of locale statements *)
+  val read_statement: Element.context list -> (string * string list) list list ->
+    Proof.context ->  (term * term list) list list * Proof.context;
+  val cert_statement: Element.context_i list -> (term * term list) list list ->
+    Proof.context -> (term * term list) list list * Proof.context;
+
   (* Declaring locales *)
   val add_locale: string -> bstring -> expression -> Element.context list -> theory ->
     string * Proof.context
@@ -27,7 +33,7 @@
 end;
 
 
-structure Expression: EXPRESSION =
+structure Expression (*: EXPRESSION *) =
 struct
 
 datatype ctxt = datatype Element.ctxt;
@@ -131,8 +137,8 @@
             val (ps, loc') = params_loc loc;
 	    val d = length ps - length insts;
 	    val insts' =
-	      if d < 0 then err_in_expr thy "More arguments than parameters in instantiation."
-                (Expr [expr])
+	      if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
+                quote (NewLocale.extern thy loc))
 	      else insts @ replicate d NONE;
             val ps' = (ps ~~ insts') |>
               map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
@@ -401,7 +407,7 @@
   let
     val thy = ProofContext.theory_of context;
 
-    fun prep_inst (loc, (prfx, inst)) (i, ids, insts, ctxt) =
+    fun prep_inst (loc, (prfx, inst)) (i, marked, insts, ctxt) =
       let
         val (parm_names, parm_types) = NewLocale.params_of thy loc |>
           map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
@@ -412,8 +418,8 @@
         val (insts'', _, _, ctxt') = check_autofix insts' [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
         val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
-        val (ids', ctxt'') = NewLocale.activate_declarations loc morph thy ids ctxt;
-      in (i+1, ids', insts', ctxt'') end;
+        val (marked', ctxt'') = NewLocale.activate_declarations thy (loc, morph) (marked, ctxt);
+      in (i+1, marked', insts', ctxt'') end;
   
     fun prep_elem raw_elem (insts, elems, ctxt) =
       let
@@ -470,7 +476,7 @@
 
 fun read_elems x = prep_elems Syntax.parse_typ Syntax.parse_prop parse_inst
   ProofContext.read_vars x;
-fun cert_elems x = prep_elems (K I) (K I) make_inst
+fun cert_elems x = prep_elems (K I) (K I)  make_inst
   ProofContext.cert_vars x;
 
 end;
@@ -480,31 +486,39 @@
 
 local
 
-fun prep_context_statement prep_expr prep_elems
+fun prep_context_statement prep_expr prep_elems activate_elems
     do_close imprt elements raw_concl context =
   let
     val thy = ProofContext.theory_of context;
 
     val (Expr expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt);
-    val ctxt = context |> ProofContext.add_fixes fixed |> snd;
-    (* FIXME push inside prep_elems *)
     val ((parms, fors, deps, elems, concl), (spec, (_, _, defs))) =
       prep_elems do_close context fixed expr elements raw_concl;
-    (* FIXME activate deps *)
-    val ((elems', _), ctxt') =
-      Element.activate elems (ProofContext.set_stmt true ctxt);
+
+    val (_, ctxt0) = ProofContext.add_fixes_i fors context;
+    val (_, ctxt) = fold (NewLocale.activate_facts thy) deps (NewLocale.empty, ctxt0);  
+    val ((elems', _), ctxt') = activate_elems elems (ProofContext.set_stmt true ctxt);
   in
     (((fors, deps), (ctxt', elems'), (parms, spec, defs)), concl)
-  end
+  end;
+
+fun prep_statement prep_ctxt elems concl ctxt =
+  let
+    val (((_, (ctxt', _), _)), concl) = prep_ctxt false (Expr [], []) elems concl ctxt
+  in (concl, ctxt') end;
 
 in
 
+fun read_statement body concl ctxt =
+  prep_statement (prep_context_statement intern read_elems Element.activate) body concl ctxt;
+fun cert_statement body concl ctxt =
+  prep_statement (prep_context_statement (K I) cert_elems Element.activate_i) body concl ctxt;
+
 fun read_context imprt body ctxt =
-  #1 (prep_context_statement intern read_elems true imprt body [] ctxt);
-(*
+  #1 (prep_context_statement intern read_elems Element.activate true imprt body [] ctxt);
 fun cert_context imprt body ctxt =
-  #1 (prep_context_statement (K I) cert_elems true imprt body [] ctxt);
-*)
+  #1 (prep_context_statement (K I) cert_elems Element.activate_i true imprt body [] ctxt);
+
 end;