src/Pure/Isar/isar_cmd.ML
changeset 7023 5d1eafaff50c
parent 7012 ae9dac5af9d1
child 7101 ee79bf6feee2
equal deleted inserted replaced
7022:abf9d5e2fb6e 7023:5d1eafaff50c
     5 Non-logical toplevel commands.
     5 Non-logical toplevel commands.
     6 *)
     6 *)
     7 
     7 
     8 signature ISAR_CMD =
     8 signature ISAR_CMD =
     9 sig
     9 sig
    10   val break: Toplevel.transition -> Toplevel.transition
       
    11   val exit: Toplevel.transition -> Toplevel.transition
    10   val exit: Toplevel.transition -> Toplevel.transition
    12   val restart: Toplevel.transition -> Toplevel.transition
    11   val restart: Toplevel.transition -> Toplevel.transition
    13   val quit: Toplevel.transition -> Toplevel.transition
    12   val quit: Toplevel.transition -> Toplevel.transition
    14   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
    13   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
    15   val clear_undo: Toplevel.transition -> Toplevel.transition
    14   val clear_undo: Toplevel.transition -> Toplevel.transition
    44 structure IsarCmd: ISAR_CMD =
    43 structure IsarCmd: ISAR_CMD =
    45 struct
    44 struct
    46 
    45 
    47 
    46 
    48 (* variations on exit *)
    47 (* variations on exit *)
    49 
       
    50 val break = Toplevel.keep (fn state => raise Toplevel.BREAK state);
       
    51 
    48 
    52 val exit = Toplevel.keep (fn state =>
    49 val exit = Toplevel.keep (fn state =>
    53   (Context.set_context (try Toplevel.theory_of state);
    50   (Context.set_context (try Toplevel.theory_of state);
    54     writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";
    51     writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";
    55     raise Toplevel.TERMINATE));
    52     raise Toplevel.TERMINATE));