tuned signature;
authorwenzelm
Wed Apr 22 19:48:32 2015 +0200 (2015-04-22 ago)
changeset 601890d3a62127057
parent 60188 b8b7006a64ef
child 60190 906de96ba68a
tuned signature;
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/toplevel.ML
src/Pure/pure_syn.ML
     1.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 22 18:43:33 2015 +0200
     1.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 22 19:48:32 2015 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  ML \<open>
     1.5    Outer_Syntax.command @{command_keyword cartouche} ""
     1.6      (Parse.cartouche >> (fn s =>
     1.7 -      Toplevel.imperative (fn () => writeln s)))
     1.8 +      Toplevel.keep (fn _ => writeln s)))
     1.9  \<close>
    1.10  
    1.11  cartouche \<open>abc\<close>
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 22 18:43:33 2015 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 22 19:48:32 2015 +0200
     2.3 @@ -854,13 +854,13 @@
     2.4  
     2.5  val _ =
     2.6    Outer_Syntax.command @{command_keyword welcome} "print welcome message"
     2.7 -    (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
     2.8 +    (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
     2.9  
    2.10  val _ =
    2.11    Outer_Syntax.command @{command_keyword display_drafts}
    2.12      "display raw source files with symbols"
    2.13      (Scan.repeat1 Parse.path >> (fn names =>
    2.14 -      Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
    2.15 +      Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
    2.16  
    2.17  
    2.18  
     3.1 --- a/src/Pure/Isar/toplevel.ML	Wed Apr 22 18:43:33 2015 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Apr 22 19:48:32 2015 +0200
     3.3 @@ -40,7 +40,6 @@
     3.4    val exit: transition -> transition
     3.5    val keep: (state -> unit) -> transition -> transition
     3.6    val keep': (bool -> state -> unit) -> transition -> transition
     3.7 -  val imperative: (unit -> unit) -> transition -> transition
     3.8    val ignored: Position.T -> transition
     3.9    val is_ignored: transition -> bool
    3.10    val malformed: Position.T -> string -> transition
    3.11 @@ -345,13 +344,12 @@
    3.12  fun transaction f = present_transaction f (K ());
    3.13  
    3.14  fun keep f = add_trans (Keep (fn _ => f));
    3.15 -fun imperative f = keep (fn _ => f ());
    3.16  
    3.17 -fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
    3.18 +fun ignored pos = empty |> name "<ignored>" |> position pos |> keep (fn _ => ());
    3.19  fun is_ignored tr = name_of tr = "<ignored>";
    3.20  
    3.21  fun malformed pos msg =
    3.22 -  empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
    3.23 +  empty |> name "<malformed>" |> position pos |> keep (fn _ => error msg);
    3.24  
    3.25  
    3.26  (* theory transitions *)
     4.1 --- a/src/Pure/pure_syn.ML	Wed Apr 22 18:43:33 2015 +0200
     4.2 +++ b/src/Pure/pure_syn.ML	Wed Apr 22 19:48:32 2015 +0200
     4.3 @@ -43,7 +43,7 @@
     4.4  
     4.5  val _ =
     4.6    Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
     4.7 -    (Parse.document_source >> K (Toplevel.imperative I));
     4.8 +    (Parse.document_source >> K (Toplevel.keep (fn _ => ())));
     4.9  
    4.10  val _ =
    4.11    Outer_Syntax.command ("theory", @{here}) "begin theory"