Corrected scheduling problem of ML*. must be atomic transaction.

src/DOF/Isa_DOF.thy

@@ -1885,18 +1885,17 @@ end;
 \<close>
 
 
-
-ML \<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/outer_syntax.ML\<close>\<close>
+\<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/outer_syntax.ML\<close>\<close>
 (*
   The ML* generates an "ontology-aware" version of the SML code-execution command.
 *)
-\<open>
+ML\<open>
 structure ML_star_Command =
 struct
 
-fun meta_args_exec NONE thy = thy
-   |meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy = 
-         thy |> (ODL_Command_Parser.create_and_check_docitem 
+fun meta_args_exec NONE  = I:generic_theory -> generic_theory
+   |meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t))  = 
+          Context.map_theory (ODL_Command_Parser.create_and_check_docitem 
                                     {is_monitor = false} {is_inline = false} 
                                     oid pos (I cid_pos) (I doc_attrs))
 
@@ -1906,12 +1905,13 @@ val _ =
   Outer_Syntax.command ("ML*", \<^here>) "ODL annotated ML text within theory or local theory"
     ((attributes_opt -- Parse.ML_source) 
      >> (fn (meta_args_opt, source) =>
-            Toplevel.theory (meta_args_exec meta_args_opt)
-            #>
+            (*Toplevel.theory (meta_args_exec meta_args_opt)
+            #>*)
             Toplevel.generic_theory
-              (ML_Context.exec (fn () =>
-                  ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
-                Local_Theory.propagate_ml_env)));
+              (ML_Context.exec (fn () =>  
+                     (ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)) 
+                  #> (meta_args_exec meta_args_opt) 
+                  #>Local_Theory.propagate_ml_env)));
 
 end
 \<close>

src/tests/Evaluation.thy

@@ -8,6 +8,17 @@ imports
   "Isabelle_DOF-tests.TermAntiquotations"
 begin
 
+section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
+ML*[the_function::C,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
+                               val t = @{const_name "List.Nil"}\<close>
+ML\<open>t\<close> \<comment> \<open>this is a test that ML* is actually evaluated and the resulting toplevel state is preserved.\<close>
+ML*\<open>3+4\<close> (* meta-args are optional *)
+
+text\<open>... and here we reference @{B [display] "the_function"}.\<close>
+
+section\<open>\<^theory_text>\<open>value*\<close>-Annotated evaluation-commands\<close>
+
+
 text\<open>The value* command uses the same code as the value command
 and adds the possibility to evaluate Term Annotation Antiquotations (TA).
 For that an elaboration of the term referenced by a TA must be done before
@@ -47,6 +58,8 @@ Here the evualuation of the TA will return the HOL.String which references the t
 \<close>
 value*\<open>@{thm \<open>HOL.refl\<close>}\<close>
 
+value*[a::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> (* using the option *)
+
 text\<open>An instance class is an object which allows us to define the concepts we want in an ontology.
 It is a concept which will be used to implement an ontology. It has roughly the same meaning as
 an individual in an OWL ontology.
@@ -155,4 +168,5 @@ to update the instance @{docitem \<open>xcv4\<close>}:
 (* Error:
 update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*)
 
+
 end