src/Pure/Isar/outer_syntax.ML
changeset 15989 80dd2f5780df
parent 15973 5fd94d84470f
child 16195 0eb3c15298cd
equal deleted inserted replaced
15988:181bbcee76f5 15989:80dd2f5780df
   370 
   370 
   371 (* main loop *)
   371 (* main loop *)
   372 
   372 
   373 fun gen_loop term no_pos =
   373 fun gen_loop term no_pos =
   374  (Context.reset_context ();
   374  (Context.reset_context ();
   375   Toplevel.loop (isar term no_pos));
   375   Toplevel.loop (isar term no_pos);
       
   376   ml_prompts "ML> " "ML# ");
   376 
   377 
   377 fun gen_main term no_pos =
   378 fun gen_main term no_pos =
   378  (Toplevel.set_state Toplevel.toplevel;
   379  (Toplevel.set_state Toplevel.toplevel;
   379   writeln (Session.welcome ());
   380   writeln (Session.welcome ());
   380   gen_loop term no_pos);
   381   gen_loop term no_pos);