src/Pure/System/isar.ML
changeset 46961 5c6955f487e5
parent 44270 3eaad39e520c
child 48646 91281e9472d8
     1.1 --- a/src/Pure/System/isar.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/Pure/System/isar.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -164,35 +164,36 @@
     1.4  (* global history *)
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
     1.8 +  Outer_Syntax.improper_command ("init_toplevel", Keyword.control) "init toplevel point-of-interest"
     1.9      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
    1.10  
    1.11  val _ =
    1.12 -  Outer_Syntax.improper_command "linear_undo" "undo commands" Keyword.control
    1.13 +  Outer_Syntax.improper_command ("linear_undo", Keyword.control) "undo commands"
    1.14      (Scan.optional Parse.nat 1 >>
    1.15        (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
    1.16  
    1.17  val _ =
    1.18 -  Outer_Syntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
    1.19 +  Outer_Syntax.improper_command ("undo", Keyword.control) "undo commands (skipping closed proofs)"
    1.20      (Scan.optional Parse.nat 1 >>
    1.21        (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
    1.22  
    1.23  val _ =
    1.24 -  Outer_Syntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
    1.25 -    Keyword.control
    1.26 +  Outer_Syntax.improper_command ("undos_proof", Keyword.control)
    1.27 +    "undo commands (skipping closed proofs)"
    1.28      (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
    1.29        Toplevel.keep (fn state =>
    1.30          if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
    1.31  
    1.32  val _ =
    1.33 -  Outer_Syntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
    1.34 -    Keyword.control
    1.35 +  Outer_Syntax.improper_command ("cannot_undo", Keyword.control)
    1.36 +    "partial undo -- Proof General legacy"
    1.37      (Parse.name >>
    1.38        (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
    1.39          | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
    1.40  
    1.41  val _ =
    1.42 -  Outer_Syntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
    1.43 +  Outer_Syntax.improper_command ("kill", Keyword.control)
    1.44 +    "kill partial proof or theory development"
    1.45      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
    1.46  
    1.47  end;