src/Pure/Isar/isar_cmd.ML
changeset 18063 c4bffc47c11b
parent 17899 0e0ac7700f57
child 18135 41cec935e804
equal deleted inserted replaced
18062:7a666583e869 18063:c4bffc47c11b
    99 val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
    99 val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
   100 val welcome = Toplevel.imperative (writeln o Session.welcome);
   100 val welcome = Toplevel.imperative (writeln o Session.welcome);
   101 
   101 
   102 val exit = Toplevel.keep (fn state =>
   102 val exit = Toplevel.keep (fn state =>
   103   (Context.set_context (try Toplevel.theory_of state);
   103   (Context.set_context (try Toplevel.theory_of state);
   104     writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";
   104     writeln "Leaving the Isar loop.  Invoke 'Isar.loop();' to continue.";
   105     raise Toplevel.TERMINATE));
   105     raise Toplevel.TERMINATE));
   106 
   106 
   107 val quit = Toplevel.imperative quit;
   107 val quit = Toplevel.imperative quit;
   108 
   108 
   109 
   109