# HG changeset patch
# User wenzelm
# Date 1207839700 -7200
# Node ID 78b3ad7af5d5e6ae5cad2b606e9a989ddbe90b15
# Parent  722cf4fdd4dd0c736cd5f70ed2845f32fb91adb9
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
tuned;

diff -r 722cf4fdd4dd -r 78b3ad7af5d5 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Apr 10 17:01:39 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Apr 10 17:01:40 2008 +0200
@@ -46,16 +46,10 @@
   type transition
   val undo_limit: bool -> int option
   val empty: transition
-  val name_of: transition -> string
-  val source_of: transition -> OuterLex.token list option
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
-  val source: OuterLex.token list -> transition -> transition
   val interactive: bool -> transition -> transition
   val print: transition -> transition
-  val print': string -> transition -> transition
-  val three_buffersN: string
-  val print3: transition -> transition
   val no_timing: transition -> transition
   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) ->
     transition -> transition
@@ -433,25 +427,21 @@
 (* datatype transition *)
 
 datatype transition = Transition of
- {name: string,                        (*command name*)
-  pos: Position.T,                     (*source position*)
-  source: OuterLex.token list option,  (*source text*)
-  int_only: bool,                      (*interactive-only*)
-  print: string list,                  (*print modes (union)*)
-  no_timing: bool,                     (*suppress timing*)
-  trans: trans list};                  (*primitive transitions (union)*)
+ {name: string,              (*command name*)
+  pos: Position.T,           (*source position*)
+  int_only: bool,            (*interactive-only*)
+  print: bool,               (*print result state*)
+  no_timing: bool,           (*suppress timing*)
+  trans: trans list};        (*primitive transitions (union)*)
 
-fun make_transition (name, pos, source, int_only, print, no_timing, trans) =
-  Transition {name = name, pos = pos, source = source,
-    int_only = int_only, print = print, no_timing = no_timing, trans = trans};
+fun make_transition (name, pos, int_only, print, no_timing, trans) =
+  Transition {name = name, pos = pos, int_only = int_only, print = print, no_timing = no_timing,
+    trans = trans};
 
-fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) =
-  make_transition (f (name, pos, source, int_only, print, no_timing, trans));
+fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) =
+  make_transition (f (name, pos, int_only, print, no_timing, trans));
 
-val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []);
-
-fun name_of (Transition {name, ...}) = name;
-fun source_of (Transition {source, ...}) = source;
+val empty = make_transition ("<unknown>", Position.none, false, false, false, []);
 
 
 (* diagnostics *)
@@ -467,31 +457,23 @@
 
 (* modify transitions *)
 
-fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) =>
-  (nm, pos, source, int_only, print, no_timing, trans));
-
-fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) =>
-  (name, pos, source, int_only, print, no_timing, trans));
+fun name nm = map_transition (fn (_, pos, int_only, print, no_timing, trans) =>
+  (nm, pos, int_only, print, no_timing, trans));
 
-fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) =>
-  (name, pos, SOME src, int_only, print, no_timing, trans));
+fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) =>
+  (name, pos, int_only, print, no_timing, trans));
 
-fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) =>
-  (name, pos, source, int_only, print, no_timing, trans));
+fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) =>
+  (name, pos, int_only, print, no_timing, trans));
 
-val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) =>
-  (name, pos, source, int_only, print, true, trans));
-
-fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
-  (name, pos, source, int_only, print, no_timing, trans @ [tr]));
+val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
+  (name, pos, int_only, print, true, trans));
 
-fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
-  (name, pos, source, int_only, insert (op =) mode print, no_timing, trans));
+fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) =>
+  (name, pos, int_only, print, no_timing, trans @ [tr]));
 
-val print = print' "";
-
-val three_buffersN = "three_buffers";
-val print3 = print' three_buffersN;
+val print = map_transition (fn (name, pos, int_only, _, no_timing, trans) =>
+  (name, pos, int_only, true, no_timing, trans));
 
 
 (* basic transitions *)
@@ -657,9 +639,7 @@
 fun app int (tr as Transition {trans, pos, int_only, print, no_timing, ...}) =
   setmp_thread_position tr (fn state =>
     let
-      val _ =
-        if not int andalso int_only then warning (command_msg "Interactive-only " tr)
-        else ();
+      val _ = if not int andalso int_only then warning (command_msg "Interactive-only " tr) else ();
 
       fun do_timing f x = (warning (command_msg "" tr); timeap f x);
       fun do_profiling f x = profile (! profiling) f x;
@@ -668,10 +648,8 @@
          state |> (apply_trans int pos trans
           |> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
           |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
-      val _ =
-        if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: print_mode_value ())
-        then print_state false result else ();
 
+      val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
     in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
 
 in