src/Pure/Isar/isar_cmd.ML
changeset 20927 2a39f2125772
parent 20803 ac78eee049ce
child 20957 f2a795db0500
equal deleted inserted replaced
20926:b2f67b947200 20927:2a39f2125772
   177 
   177 
   178 (*ignore result theory context*)
   178 (*ignore result theory context*)
   179 fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
   179 fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
   180   (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
   180   (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
   181 
   181 
   182 (*commit is dynamically bound!*)
   182 val use_commit = Toplevel.imperative Secure.commit;
   183 val use_commit = use_mltext false "commit();";
       
   184 
   183 
   185 
   184 
   186 (* current working directory *)
   185 (* current working directory *)
   187 
   186 
   188 fun cd path = Toplevel.imperative (fn () => (File.cd path));
   187 fun cd path = Toplevel.imperative (fn () => (File.cd path));