discontinued obsolete Isar.context() -- long superseded by @{context};
authorwenzelm
Thu Jun 03 22:31:59 2010 +0200 (2010-06-03 ago)
changeset 373062bde06a2a706
parent 37305 9763792e4ac7
child 37307 6dce93f3157d
discontinued obsolete Isar.context() -- long superseded by @{context};
doc-src/IsarImplementation/Thy/Integration.thy
doc-src/IsarImplementation/Thy/document/Integration.tex
src/Pure/System/isar.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/Integration.thy	Thu Jun 03 22:17:36 2010 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Integration.thy	Thu Jun 03 22:31:59 2010 +0200
     1.3 @@ -274,7 +274,6 @@
     1.4    @{index_ML Isar.loop: "unit -> unit"} \\
     1.5    @{index_ML Isar.state: "unit -> Toplevel.state"} \\
     1.6    @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
     1.7 -  @{index_ML Isar.context: "unit -> Proof.context"} \\
     1.8    @{index_ML Isar.goal: "unit ->
     1.9    {context: Proof.context, facts: thm list, goal: thm}"} \\
    1.10    \end{mldecls}
    1.11 @@ -291,10 +290,6 @@
    1.12    toplevel state and error condition, respectively.  This only works
    1.13    after having dropped out of the Isar toplevel loop.
    1.14  
    1.15 -  \item @{ML "Isar.context ()"} produces the proof context from @{ML
    1.16 -  "Isar.state ()"}, analogous to @{ML Context.proof_of}
    1.17 -  (\secref{sec:generic-context}).
    1.18 -
    1.19    \item @{ML "Isar.goal ()"} produces the full Isar goal state,
    1.20    consisting of proof context, facts that have been indicated for
    1.21    immediate use, and the tactical goal according to
     2.1 --- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Jun 03 22:17:36 2010 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Thu Jun 03 22:31:59 2010 +0200
     2.3 @@ -335,7 +335,6 @@
     2.4    \indexdef{}{ML}{Isar.loop}\verb|Isar.loop: unit -> unit| \\
     2.5    \indexdef{}{ML}{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
     2.6    \indexdef{}{ML}{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
     2.7 -  \indexdef{}{ML}{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
     2.8    \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit ->|\isasep\isanewline%
     2.9  \verb|  {context: Proof.context, facts: thm list, goal: thm}| \\
    2.10    \end{mldecls}
    2.11 @@ -352,9 +351,6 @@
    2.12    toplevel state and error condition, respectively.  This only works
    2.13    after having dropped out of the Isar toplevel loop.
    2.14  
    2.15 -  \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
    2.16 -  (\secref{sec:generic-context}).
    2.17 -
    2.18    \item \verb|Isar.goal ()| produces the full Isar goal state,
    2.19    consisting of proof context, facts that have been indicated for
    2.20    immediate use, and the tactical goal according to
     3.1 --- a/src/Pure/System/isar.ML	Thu Jun 03 22:17:36 2010 +0200
     3.2 +++ b/src/Pure/System/isar.ML	Thu Jun 03 22:31:59 2010 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      Pure/System/isar.ML
     3.5      Author:     Makarius
     3.6  
     3.7 -The global Isabelle/Isar state and main read-eval-print loop.
     3.8 +Global state of the raw Isar read-eval-print loop.
     3.9  *)
    3.10  
    3.11  signature ISAR =
    3.12 @@ -9,7 +9,6 @@
    3.13    val init: unit -> unit
    3.14    val exn: unit -> (exn * string) option
    3.15    val state: unit -> Toplevel.state
    3.16 -  val context: unit -> Proof.context
    3.17    val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
    3.18    val print: unit -> unit
    3.19    val >> : Toplevel.transition -> bool
    3.20 @@ -57,9 +56,6 @@
    3.21  
    3.22  fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
    3.23  
    3.24 -fun context () = Toplevel.context_of (state ())
    3.25 -  handle Toplevel.UNDEF => error "Unknown context";
    3.26 -
    3.27  fun goal () = Proof.goal (Toplevel.proof_of (state ()))
    3.28    handle Toplevel.UNDEF => error "No goal present";
    3.29