Isar.init;
authorwenzelm
Mon Jan 05 00:13:11 2009 +0100 (2009-01-05)
changeset 29349b49d8501720a
parent 29348 28b0652aabd8
child 29350 c7735554d291
Isar.init;
src/Pure/Isar/isar_syn.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Jan 05 00:12:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Jan 05 00:13:11 2009 +0100
     1.3 @@ -774,7 +774,7 @@
     1.4  
     1.5  val _ =
     1.6    OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
     1.7 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init_point));
     1.8 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init));
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.improper_command "linear_undo" "undo commands" K.control
     2.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jan 05 00:12:49 2009 +0100
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jan 05 00:13:11 2009 +0100
     2.3 @@ -144,7 +144,7 @@
     2.4              (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
     2.5                tell_file_retracted (ThyLoad.thy_path name))
     2.6        else ();
     2.7 -    val _ = Isar.init_point ();
     2.8 +    val _ = Isar.init ();
     2.9    in () end;
    2.10  
    2.11  
    2.12 @@ -156,7 +156,7 @@
    2.13   (sync_thy_loader ();
    2.14    tell_clear_goals ();
    2.15    tell_clear_response ();
    2.16 -  Isar.init_point ();
    2.17 +  Isar.init ();
    2.18    welcome ());
    2.19  
    2.20  
     3.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jan 05 00:12:49 2009 +0100
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jan 05 00:13:11 2009 +0100
     3.3 @@ -242,7 +242,7 @@
     3.4      (sync_thy_loader ();
     3.5       tell_clear_goals ();
     3.6       tell_clear_response ();
     3.7 -     Isar.init_point ();
     3.8 +     Isar.init ();
     3.9       welcome ());
    3.10  
    3.11