src/Pure/Isar/isar_cmd.ML
changeset 7891 c77ad0c3c92f
parent 7790 2fd4d53acc0a
child 7908 0b191b36ad97
equal deleted inserted replaced
7890:0aa16bc2abdb 7891:c77ad0c3c92f
    21   val kill_proof: Toplevel.transition -> Toplevel.transition
    21   val kill_proof: Toplevel.transition -> Toplevel.transition
    22   val undo_theory: Toplevel.transition -> Toplevel.transition
    22   val undo_theory: Toplevel.transition -> Toplevel.transition
    23   val undo: Toplevel.transition -> Toplevel.transition
    23   val undo: Toplevel.transition -> Toplevel.transition
    24   val use: string -> Toplevel.transition -> Toplevel.transition
    24   val use: string -> Toplevel.transition -> Toplevel.transition
    25   val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
    25   val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
    26   val use_mltext: string -> Toplevel.transition -> Toplevel.transition
    26   val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
    27   val use_commit: Toplevel.transition -> Toplevel.transition
    27   val use_commit: Toplevel.transition -> Toplevel.transition
    28   val cd: string -> Toplevel.transition -> Toplevel.transition
    28   val cd: string -> Toplevel.transition -> Toplevel.transition
    29   val pwd: Toplevel.transition -> Toplevel.transition
    29   val pwd: Toplevel.transition -> Toplevel.transition
    30   val use_thy: string -> Toplevel.transition -> Toplevel.transition
    30   val use_thy: string -> Toplevel.transition -> Toplevel.transition
    31   val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
    31   val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
    98 
    98 
    99 (*passes changes of theory context*)
    99 (*passes changes of theory context*)
   100 val use_mltext_theory = Toplevel.theory' o IsarThy.use_mltext_theory;
   100 val use_mltext_theory = Toplevel.theory' o IsarThy.use_mltext_theory;
   101 
   101 
   102 (*ignore result theory context*)
   102 (*ignore result theory context*)
   103 fun use_mltext txt = Toplevel.keep' (fn verb => fn state =>
   103 fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
   104   (IsarThy.use_mltext txt verb (try Toplevel.theory_of state)));
   104   (IsarThy.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
   105 
   105 
   106 (*Note: commit is dynamically bound*)
   106 (*Note: commit is dynamically bound*)
   107 val use_commit = use_mltext "commit();";
   107 val use_commit = use_mltext false "commit();";
   108 
   108 
   109 
   109 
   110 (* current working directory *)
   110 (* current working directory *)
   111 
   111 
   112 fun cd dir = Toplevel.imperative (fn () => (File.cd (Path.unpack dir)));
   112 fun cd dir = Toplevel.imperative (fn () => (File.cd (Path.unpack dir)));