src/Pure/Isar/isar_thy.ML
changeset 6266 a5f9fa6b6d7c
parent 6253 dbaf79ac2ff9
child 6331 fb7b8d6c2bd1
equal deleted inserted replaced
6265:aaabe48bafcb 6266:a5f9fa6b6d7c
   172 val default_proof = ProofHistory.applys_close Method.default_proof;
   172 val default_proof = ProofHistory.applys_close Method.default_proof;
   173 
   173 
   174 
   174 
   175 (* use ML text *)
   175 (* use ML text *)
   176 
   176 
   177 fun use_mltext txt opt_thy =
   177 fun use_mltext txt opt_thy = #2 (Context.fetch opt_thy (use_text false) txt);
   178   let
   178 fun use_mltext_theory txt thy = #2 (Context.fetch_theory thy (use_text false) txt);
   179     val save_context = Context.get_context ();
       
   180     val _ = Context.set_context opt_thy;
       
   181     val opt_exn = (transform_error (use_text false) txt; None) handle exn => Some exn;
       
   182     val opt_thy' = Context.get_context ();
       
   183   in
       
   184     Context.set_context save_context;
       
   185     (case opt_exn of
       
   186       None => opt_thy'
       
   187     | Some exn => raise exn)
       
   188   end;
       
   189 
       
   190 fun use_mltext_theory txt thy =
       
   191   (case use_mltext txt (Some thy) of
       
   192     Some thy' => thy'
       
   193   | None => error "Missing result ML theory context");
       
   194 
       
   195 
   179 
   196 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");");
   180 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");");
   197 
   181 
   198 fun use_let name body txt =
   182 fun use_let name body txt =
   199   use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   183   use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   239 
   223 
   240 
   224 
   241 (* theory init and exit *)
   225 (* theory init and exit *)
   242 
   226 
   243 fun begin_theory (name, parents, files) () =
   227 fun begin_theory (name, parents, files) () =
   244   let val thy = ThyInfo.begin_theory name parents
   228   let
   245   in seq ThyInfo.use (mapfilter (fn (x, true) => Some x | _ => None) files); thy end;
   229     val thy = ThyInfo.begin_theory name parents;
       
   230     val names = mapfilter (fn (x, true) => Some x | _ => None) files;
       
   231   in Context.setmp (Some thy) (seq ThyInfo.use) names; thy end;
   246 
   232 
   247 fun end_theory thy =
   233 fun end_theory thy =
   248   let val thy' = PureThy.end_theory thy in
   234   let val thy' = PureThy.end_theory thy in
   249     transform_error ThyInfo.put_theory thy'
   235     transform_error ThyInfo.put_theory thy'
   250       handle exn => raise PureThy.ROLLBACK (thy', Some exn)     (* FIXME !!?? *)
   236       handle exn => raise PureThy.ROLLBACK (thy', Some exn)     (* FIXME !!?? *)