Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
authorhaftmann
Mon Jan 21 07:08:27 2019 +0000 (5 months ago ago)
changeset 697241c201e4792cb
parent 69723 920fe0a2fd22
child 69725 7263b59219c1
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
NEWS
src/Pure/Isar/local_theory.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/NEWS	Mon Jan 21 22:46:25 2019 +0100
     1.2 +++ b/NEWS	Mon Jan 21 07:08:27 2019 +0000
     1.3 @@ -134,6 +134,11 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Local_Theory.reset is no longer available in user space. Regular
     1.8 +definitional packages should use balanced blocks of
     1.9 +Local_Theory.open_target versus Local_Theory.close_target instead,
    1.10 +or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
    1.11 +
    1.12  * Original PolyML.pointerEq is retained as a convenience for tools that
    1.13  don't use Isabelle/ML (where this is called "pointer_eq").
    1.14  
     2.1 --- a/src/Pure/Isar/local_theory.ML	Mon Jan 21 22:46:25 2019 +0100
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Mon Jan 21 07:08:27 2019 +0000
     2.3 @@ -23,7 +23,6 @@
     2.4  sig
     2.5    type operations
     2.6    val assert: local_theory -> local_theory
     2.7 -  val reset: local_theory -> local_theory
     2.8    val level: Proof.context -> int
     2.9    val assert_bottom: local_theory -> local_theory
    2.10    val mark_brittle: local_theory -> local_theory
    2.11 @@ -83,7 +82,13 @@
    2.12      local_theory -> 'b * local_theory
    2.13  end;
    2.14  
    2.15 -structure Local_Theory: LOCAL_THEORY =
    2.16 +signature PRIVATE_LOCAL_THEORY =
    2.17 +sig
    2.18 +  include LOCAL_THEORY
    2.19 +  val reset: local_theory -> local_theory
    2.20 +end
    2.21 +
    2.22 +structure Local_Theory: PRIVATE_LOCAL_THEORY =
    2.23  struct
    2.24  
    2.25  (** local theory data **)
     3.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jan 21 22:46:25 2019 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jan 21 07:08:27 2019 +0000
     3.3 @@ -749,3 +749,5 @@
     3.4  end;
     3.5  
     3.6  end;
     3.7 +
     3.8 +structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end;