# HG changeset patch
# User Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
# Date 1535460340 -3600
# Node ID 43334463428a2be4617706a5bcdf029d5d73b26e
# Parent  fde093888c16ae52cd22298a9a5e201d3a9a734d# Parent  9b9fc9ea9dd1624bd95a6748b520eee1934b57e7
merged

diff -r fde093888c16 -r 43334463428a src/HOL/Real_Asymp/real_asymp_diag.ML
--- a/src/HOL/Real_Asymp/real_asymp_diag.ML	Tue Aug 28 13:28:39 2018 +0100
+++ b/src/HOL/Real_Asymp/real_asymp_diag.ML	Tue Aug 28 13:45:40 2018 +0100
@@ -187,7 +187,7 @@
   end
 
 fun print_basis_elem ctxt t =
-  Syntax.pretty_term (Config.put Syntax_Trans.eta_contract_raw (Config.Bool false) ctxt)
+  Syntax.pretty_term (Config.put Syntax_Trans.eta_contract false ctxt)
     (Envir.eta_long [] t)
 
 val expansion_cmd =
diff -r fde093888c16 -r 43334463428a src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Aug 28 13:28:39 2018 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Aug 28 13:45:40 2018 +0100
@@ -1490,7 +1490,7 @@
 ML \<open>
 fun remove_duplicates_tac feats =
   (if can_feature (CleanUp [RemoveDuplicates]) feats then
-     ALLGOALS distinct_subgoal_tac
+     distinct_subgoals_tac
    else all_tac)
 \<close>
 
diff -r fde093888c16 -r 43334463428a src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Aug 28 13:28:39 2018 +0100
+++ b/src/Pure/General/position.ML	Tue Aug 28 13:45:40 2018 +0100
@@ -29,6 +29,7 @@
   val id_only: string -> T
   val get_id: T -> string option
   val put_id: string -> T -> T
+  val id_properties_of: T -> Properties.T
   val parse_id: T -> int option
   val adjust_offsets: (int -> int option) -> T -> T
   val of_properties: Properties.T -> T
@@ -144,6 +145,10 @@
 
 fun parse_id pos = Option.map Value.parse_int (get_id pos);
 
+fun id_properties_of pos =
+  (case get_id pos of
+    SOME id => [(Markup.idN, id)]
+  | NONE => []);
 
 fun adjust_offsets adjust (pos as Pos (_, props)) =
   (case parse_id pos of
diff -r fde093888c16 -r 43334463428a src/Pure/PIDE/active.ML
--- a/src/Pure/PIDE/active.ML	Tue Aug 28 13:28:39 2018 +0100
+++ b/src/Pure/PIDE/active.ML	Tue Aug 28 13:45:40 2018 +0100
@@ -21,10 +21,7 @@
 
 (* active markup *)
 
-fun explicit_id () =
-  (case Position.get_id (Position.thread_data ()) of
-    SOME id => [(Markup.idN, id)]
-  | NONE => []);
+fun explicit_id () = Position.id_properties_of (Position.thread_data ());
 
 fun make_markup name {implicit, properties} =
   (name, [])
diff -r fde093888c16 -r 43334463428a src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Aug 28 13:28:39 2018 +0100
+++ b/src/Pure/Pure.thy	Tue Aug 28 13:45:40 2018 +0100
@@ -196,11 +196,12 @@
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory (fn context =>
         context
+        |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle
         |> Config.put_generic ML_Env.ML_write_global true
         |> ML_Context.exec (fn () =>
             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
-        |> Config.put_generic ML_Env.ML_write_global
-            (Config.get_generic context ML_Env.ML_write_global)
+        |> Config.restore_generic ML_Env.ML_write_global context
+        |> Config.restore_generic ML_Env.ML_environment context
         |> Local_Theory.propagate_ml_env)));
 
 val _ =
diff -r fde093888c16 -r 43334463428a src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Aug 28 13:28:39 2018 +0100
+++ b/src/Pure/Thy/export.scala	Tue Aug 28 13:45:40 2018 +0100
@@ -150,6 +150,16 @@
     })
   }
 
+  def read_entry(dir: Path, session_name: String, theory_name: String, name: String): Option[Entry] =
+  {
+    val path = dir + Path.basic(theory_name) + Path.explode(name)
+    if (path.is_file) {
+      val uncompressed = Bytes.read(path)
+      Some(Entry(session_name, theory_name, name, Future.value((false, uncompressed))))
+    }
+    else None
+  }
+
 
   /* database consumer thread */
 
@@ -193,12 +203,24 @@
       new Provider {
         def apply(export_name: String): Option[Entry] =
           read_entry(db, session_name, theory_name, export_name)
+
+        override def toString: String = db.toString
       }
 
     def snapshot(snapshot: Document.Snapshot): Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] =
           snapshot.exports_map.get(export_name)
+
+        override def toString: String = snapshot.toString
+      }
+
+    def directory(dir: Path, session_name: String, theory_name: String): Provider =
+      new Provider {
+        def apply(export_name: String): Option[Entry] =
+          read_entry(dir, session_name, theory_name, export_name)
+
+        override def toString: String = dir.toString
       }
   }
 
diff -r fde093888c16 -r 43334463428a src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Tue Aug 28 13:28:39 2018 +0100
+++ b/src/Pure/Thy/export_theory.ML	Tue Aug 28 13:45:40 2018 +0100
@@ -66,8 +66,9 @@
       let
         val {serial, pos, ...} = Name_Space.the_entry space name;
         val props =
-          Markup.serial_properties serial @
-          Position.offset_properties_of (adjust_pos pos);
+          Position.offset_properties_of (adjust_pos pos) @
+          Position.id_properties_of pos @
+          Markup.serial_properties serial;
       in (Markup.entityN, (Markup.nameN, name) :: props) end;
 
     fun export_entities export_name export get_space decls =
diff -r fde093888c16 -r 43334463428a src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Aug 28 13:28:39 2018 +0100
+++ b/src/Pure/Thy/export_theory.scala	Tue Aug 28 13:45:40 2018 +0100
@@ -156,12 +156,12 @@
     val CLASS = Value("class")
   }
 
-  sealed case class Entity(kind: Kind.Value, name: String, serial: Long, pos: Position.T)
+  sealed case class Entity(kind: Kind.Value, name: String, pos: Position.T, id: Long, serial: Long)
   {
     override def toString: String = kind.toString + " " + quote(name)
 
     def cache(cache: Term.Cache): Entity =
-      Entity(kind, cache.string(name), serial, cache.position(pos))
+      Entity(kind, cache.string(name), cache.position(pos), id, serial)
   }
 
   def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
@@ -171,9 +171,10 @@
     tree match {
       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
         val name = Markup.Name.unapply(props) getOrElse err()
+        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
+        val id = Position.Id.unapply(props) getOrElse err()
         val serial = Markup.Serial.unapply(props) getOrElse err()
-        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
-        (Entity(kind, name, serial, pos), body)
+        (Entity(kind, name, pos, id, serial), body)
       case _ => err()
     }
   }
diff -r fde093888c16 -r 43334463428a src/Pure/config.ML
--- a/src/Pure/config.ML	Tue Aug 28 13:28:39 2018 +0100
+++ b/src/Pure/config.ML	Tue Aug 28 13:45:40 2018 +0100
@@ -18,12 +18,15 @@
   val get: Proof.context -> 'a T -> 'a
   val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
   val put: 'a T -> 'a -> Proof.context -> Proof.context
+  val restore: 'a T -> Proof.context -> Proof.context -> Proof.context
   val get_global: theory -> 'a T -> 'a
   val map_global: 'a T -> ('a -> 'a) -> theory -> theory
   val put_global: 'a T -> 'a -> theory -> theory
+  val restore_global: 'a T -> theory -> theory -> theory
   val get_generic: Context.generic -> 'a T -> 'a
   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
+  val restore_generic: 'a T -> Context.generic -> Context.generic -> Context.generic
   val declare: string * Position.T -> (Context.generic -> value) -> raw
   val declare_option: string * Position.T -> raw
   val name_of: 'a T -> string
@@ -91,14 +94,17 @@
 fun get_generic context (Config {get_value, ...}) = get_value context;
 fun map_generic (Config {map_value, ...}) f context = map_value f context;
 fun put_generic config value = map_generic config (K value);
+fun restore_generic config context = put_generic config (get_generic context config);
 
 fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
 fun map_ctxt config f = Context.proof_map (map_generic config f);
 fun put_ctxt config value = map_ctxt config (K value);
+fun restore_ctxt config ctxt = put_ctxt config (get_ctxt ctxt config);
 
 fun get_global thy = get_generic (Context.Theory thy);
 fun map_global config f = Context.theory_map (map_generic config f);
 fun put_global config value = map_global config (K value);
+fun restore_global config thy = put_global config (get_global thy config);
 
 
 (* context information *)
@@ -145,5 +151,6 @@
 val get = get_ctxt;
 val map = map_ctxt;
 val put = put_ctxt;
+val restore = restore_ctxt;
 
 end;
diff -r fde093888c16 -r 43334463428a src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Aug 28 13:28:39 2018 +0100
+++ b/src/Pure/tactic.ML	Tue Aug 28 13:45:40 2018 +0100
@@ -28,7 +28,6 @@
   val ematch_tac: Proof.context -> thm list -> int -> tactic
   val dmatch_tac: Proof.context -> thm list -> int -> tactic
   val flexflex_tac: Proof.context -> tactic
-  val distinct_subgoal_tac: int -> tactic
   val distinct_subgoals_tac: tactic
   val cut_tac: thm -> int -> tactic
   val cut_rules_tac: thm list -> int -> tactic