# HG changeset patch
# User wenzelm
# Date 972423377 -7200
# Node ID bbaad3045e378067307c1067dd5ab4c2c17e2a7e
# Parent  26d4b84eb04717e53aa39d480cb30b9d835eea35
let commands access Toplevel.state;
added command "goals" and option "goals_limit";

diff -r 26d4b84eb047 -r bbaad3045e37 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Tue Oct 24 23:35:29 2000 +0200
+++ b/src/Pure/Isar/isar_output.ML	Tue Oct 24 23:36:17 2000 +0200
@@ -8,13 +8,13 @@
 
 signature ISAR_OUTPUT =
 sig
-  val add_commands: (string * (Args.src -> Proof.context -> string)) list -> unit
+  val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
   val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
   val print_antiquotations: unit -> unit
   val boolean: string -> bool
   val integer: string -> int
   val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
-    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Proof.context -> string
+    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
   datatype markup = Markup | MarkupEnv | Verbatim
   val interest_level: int ref
   val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) ->
@@ -38,7 +38,7 @@
 local
 
 val global_commands =
-  ref (Symtab.empty: (Args.src -> Proof.context -> string) Symtab.table);
+  ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
 
 val global_options =
   ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
@@ -102,9 +102,9 @@
 fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
   Args.syntax "antiquotation" scan;
 
-fun args scan f src ctxt : string =
-  let val (ctxt', x) = syntax scan src ctxt
-  in f src ctxt' x end;
+fun args scan f src state : string =
+  let val (ctxt, x) = syntax scan src (Toplevel.context_of state)
+  in f src ctxt x end;
 
 
 (* outer syntax *)
@@ -141,8 +141,8 @@
     fun expand (Antiquote.Text s) = s
       | expand (Antiquote.Antiq x) =
           let val (opts, src) = antiq_args lex x in
-            Library.setmp print_mode Latex.modes   (*note: lazy lookup of context below!*)
-              (options opts (fn () => command src (Toplevel.context_of state))) () end;
+            Library.setmp print_mode Latex.modes (options opts (fn () => command src state)) ()
+          end;
     val ants = Antiquote.antiquotes_of (str, pos);
   in
     if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
@@ -258,7 +258,8 @@
   ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
   ("margin", Pretty.setmp_margin o integer),
   ("indent", Library.setmp indent o integer),
-  ("source", Library.setmp source o boolean)];
+  ("source", Library.setmp source o boolean),
+  ("goals_limit", Library.setmp goals_limit o integer)];
 
 
 (* commands *)
@@ -291,6 +292,9 @@
 fun pretty_thm ctxt thms =
   Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms);
 
+fun pretty_goals state _ _ =
+  Pretty.chunks (Proof.pretty_goals (Toplevel.proof_of state));
+
 
 fun output_with pretty src ctxt x =
   let
@@ -305,7 +309,9 @@
   ("thm", args Attrib.local_thms (output_with pretty_thm)),
   ("prop", args Args.local_prop (output_with pretty_term)),
   ("term", args Args.local_term (output_with pretty_term)),
-  ("typ", args Args.local_typ_no_norm (output_with pretty_typ))];
+  ("typ", args Args.local_typ_no_norm (output_with pretty_typ)),
+  ("goals", fn src => fn state =>
+      args (Scan.succeed ()) (output_with (pretty_goals state)) src state)];
 
 end;