--- 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 =
--- 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>
--- 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
--- 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, [])
--- 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 _ =
--- 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
}
}
--- 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 =
--- 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()
}
}
--- 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;
--- 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