# HG changeset patch # User Angeliki KoutsoukouArgyraki # 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 \ fun remove_duplicates_tac feats = (if can_feature (CleanUp [RemoveDuplicates]) feats then - ALLGOALS distinct_subgoal_tac + distinct_subgoals_tac else all_tac) \ 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