# HG changeset patch # User Christian Urban # Date 1244168248 -7200 # Node ID 5accec94b6dff1db2dcdef4d1bb047ccd222d54f # Parent a0af7fe3f558737a6c82869e59507c0c2cd84fd2 updated to lates Isabelle changes diff -r a0af7fe3f558 -r 5accec94b6df ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Thu Jun 04 09:28:29 2009 +0200 +++ b/ProgTutorial/Base.thy Fri Jun 05 04:17:28 2009 +0200 @@ -9,27 +9,26 @@ (* to have a special tag for text enclosed in ML *) ML {* -fun inherit_env (context as Context.Proof lthy) = - Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy) - | inherit_env context = context; +fun propagate_env (context as Context.Proof lthy) = + Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) + | propagate_env context = context; -fun inherit_env_prf prf = Proof.map_contexts - (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf +fun propagate_env_prf prf = Proof.map_contexts + (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf; val _ = OuterSyntax.command "ML" "eval ML text within theory" (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) (OuterParse.ML_source >> (fn (txt, pos) => Toplevel.generic_theory - (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env))); - + (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env))); val _ = OuterSyntax.command "ML_prf" "ML text within proof" (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) (OuterParse.ML_source >> (fn (txt, pos) => Toplevel.proof (Proof.map_context (Context.proof_map - (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf))) + (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) val _ = OuterSyntax.command "ML_val" "diagnostic ML text" diff -r a0af7fe3f558 -r 5accec94b6df ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Thu Jun 04 09:28:29 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Fri Jun 05 04:17:28 2009 +0200 @@ -122,7 +122,7 @@ @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} - However, @{ML [index] makestring} only works if the type of what is converted is monomorphic + However, @{ML [index] makestring in PolyML} only works if the type of what is converted is monomorphic and not a function. The function @{ML "writeln"} should only be used for testing purposes, because any diff -r a0af7fe3f558 -r 5accec94b6df progtutorial.pdf Binary file progtutorial.pdf has changed