Isar.toplevel_loop: separate init/welcome flag;
authorwenzelm
Mon Apr 14 14:28:47 2008 +0200 (2008-04-14)
changeset 2664399f5407c05ef
parent 26642 454d11701fa4
child 26644 2f12191282e2
Isar.toplevel_loop: separate init/welcome flag;
src/Pure/Isar/isar.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/Tools/isabelle_process.ML
     1.1 --- a/src/Pure/Isar/isar.ML	Sun Apr 13 16:40:08 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar.ML	Mon Apr 14 14:28:47 2008 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val >>> : Toplevel.transition list -> unit
     1.5    val init: unit -> unit
     1.6    val crashes: exn list ref
     1.7 -  val toplevel_loop: {init: bool, sync: bool, secure: bool} -> unit
     1.8 +  val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
     1.9    val loop: unit -> unit
    1.10    val main: unit -> unit
    1.11  end;
    1.12 @@ -81,15 +81,18 @@
    1.13  
    1.14  in
    1.15  
    1.16 -fun toplevel_loop {init = do_init, sync, secure} =
    1.17 +fun toplevel_loop {init = do_init, welcome, sync, secure} =
    1.18   (Context.set_thread_data NONE;
    1.19 -  if do_init then (init (); writeln (Session.welcome ())) else ();
    1.20 +  if do_init then init () else ();
    1.21 +  if welcome then writeln (Session.welcome ()) else ();
    1.22    uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
    1.23  
    1.24  end;
    1.25  
    1.26 -fun loop () = toplevel_loop {init = false, sync = false, secure = Secure.is_secure ()};
    1.27 -fun main () = toplevel_loop {init = true, sync = false, secure = Secure.is_secure ()};
    1.28 +fun loop () =
    1.29 +  toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
    1.30 +fun main () =
    1.31 +  toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
    1.32  
    1.33  end;
    1.34  
     2.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun Apr 13 16:40:08 2008 +0200
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Apr 14 14:28:47 2008 +0200
     2.3 @@ -297,6 +297,6 @@
     2.4            set initialized);
     2.5          sync_thy_loader ();
     2.6         change print_mode (update (op =) proof_generalN);
     2.7 -       Isar.toplevel_loop {init = true, sync = true, secure = Secure.is_secure ()});
     2.8 +       Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
     2.9  
    2.10  end;
     3.1 --- a/src/Pure/Tools/isabelle_process.ML	Sun Apr 13 16:40:08 2008 +0200
     3.2 +++ b/src/Pure/Tools/isabelle_process.ML	Mon Apr 14 14:28:47 2008 +0200
     3.3 @@ -155,7 +155,7 @@
     3.4   (change print_mode (update (op =) isabelle_processN);
     3.5    setup_channels ();
     3.6    init_message ();
     3.7 -  Isar.toplevel_loop {init = true, sync = true, secure = true});
     3.8 +  Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
     3.9  
    3.10  end;
    3.11