src/Pure/Isar/isar_syn.ML
changeset 30703 a1a47e653eb7
parent 30579 4169ddbfe1f9
child 30727 519f8f0fcbf3
equal deleted inserted replaced
30702:274626e2b2dd 30703:a1a47e653eb7
   293       (Toplevel.theory o uncurry IsarCmd.hide_names));
   293       (Toplevel.theory o uncurry IsarCmd.hide_names));
   294 
   294 
   295 
   295 
   296 (* use ML text *)
   296 (* use ML text *)
   297 
   297 
   298 fun inherit_env (context as Context.Proof lthy) =
   298 fun propagate_env (context as Context.Proof lthy) =
   299       Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
   299       Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
   300   | inherit_env context = context;
   300   | propagate_env context = context;
   301 
   301 
   302 fun inherit_env_prf prf = Proof.map_contexts
   302 fun propagate_env_prf prf = Proof.map_contexts
   303   (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
   303   (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
   304 
   304 
   305 val _ =
   305 val _ =
   306   OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
   306   OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
   307     (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> inherit_env)));
   307     (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
   308 
   308 
   309 val _ =
   309 val _ =
   310   OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl)
   310   OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl)
   311     (P.ML_source >> (fn (txt, pos) =>
   311     (P.ML_source >> (fn (txt, pos) =>
   312       Toplevel.generic_theory
   312       Toplevel.generic_theory
   313         (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env)));
   313         (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
   314 
   314 
   315 val _ =
   315 val _ =
   316   OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl)
   316   OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl)
   317     (P.ML_source >> (fn (txt, pos) =>
   317     (P.ML_source >> (fn (txt, pos) =>
   318       Toplevel.proof (Proof.map_context (Context.proof_map
   318       Toplevel.proof (Proof.map_context (Context.proof_map
   319         (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)));
   319         (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)));
   320 
   320 
   321 val _ =
   321 val _ =
   322   OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag)
   322   OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag)
   323     (P.ML_source >> IsarCmd.ml_diag true);
   323     (P.ML_source >> IsarCmd.ml_diag true);
   324 
   324