# HG changeset patch # User wenzelm # Date 1526241581 -7200 # Node ID 7c4793e39dd54d797d87c554bd3d2f804c932f03 # Parent 61878d2aa6c7a8b67d47ec10b236f6b803a3d199# Parent 7ed88a534bb6bd2be738100912df961310e841c0 merged diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/Admin/build_log.scala Sun May 13 21:59:41 2018 +0200 @@ -253,7 +253,7 @@ /* properties (YXML) */ - val xml_cache = new XML.Cache() + val xml_cache = XML.make_cache() def parse_props(text: String): Properties.T = try { @@ -881,7 +881,7 @@ class Store private[Build_Log](options: Options) { - val xml_cache: XML.Cache = new XML.Cache() + val xml_cache: XML.Cache = XML.make_cache() val xz_cache: XZ.Cache = XZ.make_cache() def open_database( diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/General/bytes.scala Sun May 13 21:59:41 2018 +0200 @@ -205,4 +205,11 @@ using(new XZOutputStream(result, options, cache))(write_stream(_)) new Bytes(result.toByteArray, 0, result.size) } + + def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()) + : (Boolean, Bytes) = + { + val compressed = compress(options = options, cache = cache) + if (compressed.length < length) (true, compressed) else (false, this) + } } diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/General/name_space.ML Sun May 13 21:59:41 2018 +0200 @@ -62,6 +62,7 @@ val alias: naming -> binding -> string -> T -> T val naming_of: Context.generic -> naming val map_naming: (naming -> naming) -> Context.generic -> Context.generic + val declared: T -> string -> bool val declare: Context.generic -> bool -> binding -> T -> string * T type 'a table val change_base: bool -> 'a table -> 'a table @@ -80,6 +81,7 @@ val del_table: string -> 'a table -> 'a table val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b + val dest_table: 'a table -> (string * 'a) list val empty_table: string -> 'a table val merge_tables: 'a table * 'a table -> 'a table val join_tables: (string -> 'a * 'a -> 'a) (*exception Change_Table.SAME*) -> @@ -503,6 +505,8 @@ (* declaration *) +fun declared (Name_Space {entries, ...}) = Change_Table.defined entries; + fun declare context strict binding space = let val naming = naming_of context; @@ -608,6 +612,7 @@ Table (space, Change_Table.map_entry name f tab); fun fold_table f (Table (_, tab)) = Change_Table.fold f tab; +fun dest_table (Table (_, tab)) = Change_Table.dest tab; fun empty_table kind = Table (empty kind, Change_Table.empty); diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/General/position.ML Sun May 13 21:59:41 2018 +0200 @@ -32,6 +32,7 @@ val parse_id: T -> int option val of_properties: Properties.T -> T val properties_of: T -> Properties.T + val offset_properties_of: T -> Properties.T val def_properties_of: T -> Properties.T val entity_properties_of: bool -> serial -> T -> Properties.T val default_properties: T -> Properties.T -> Properties.T @@ -161,6 +162,9 @@ fun properties_of (Pos ((i, j, k), props)) = value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props; +fun offset_properties_of (Pos ((_, j, k), _)) = + value Markup.offsetN j @ value Markup.end_offsetN k; + val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y)); fun entity_properties_of def serial pos = diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/PIDE/session.scala Sun May 13 21:59:41 2018 +0200 @@ -118,7 +118,8 @@ { session => - val xml_cache: XML.Cache = new XML.Cache() + val xml_cache: XML.Cache = XML.make_cache() + val xz_cache: XZ.Cache = XZ.make_cache() /* global flags */ @@ -436,8 +437,8 @@ case Markup.Export(args) if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => val id = Value.Long.unapply(args.id.get).get - val entry = (args.serial, Export.make_entry("", args, msg.bytes)) - change_command(_.add_export(id, entry)) + val export = Export.make_entry("", args, msg.bytes, cache = xz_cache) + change_command(_.add_export(id, (args.serial, export))) case Markup.Assign_Update => msg.text match { diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/PIDE/xml.scala Sun May 13 21:59:41 2018 +0200 @@ -154,7 +154,10 @@ /** cache for partial sharing (weak table) **/ - class Cache(initial_size: Int = 131071, max_string: Int = 100) + def make_cache(initial_size: Int = 131071, max_string: Int = 100): Cache = + new Cache(initial_size, max_string) + + class Cache private[XML](initial_size: Int, max_string: Int) { private val table = Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size)) diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/System/isabelle_process.scala Sun May 13 21:59:41 2018 +0200 @@ -42,7 +42,7 @@ cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true), - xml_cache: XML.Cache = new XML.Cache(), + xml_cache: XML.Cache = XML.make_cache(), sessions: Option[Sessions.Structure] = None, store: Sessions.Store = Sessions.store()): Prover = { diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/Thy/export.ML Sun May 13 21:59:41 2018 +0200 @@ -33,7 +33,7 @@ name = check_name name, compress = compress} body; -fun export thy name body = gen_export (fold (Integer.add o size) body 0 > 60) thy name body; +val export = gen_export true; val export_raw = gen_export false; end; diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/Thy/export.scala Sun May 13 21:59:41 2018 +0200 @@ -63,14 +63,13 @@ session_name: String, theory_name: String, name: String, - compressed: Boolean, - body: Future[Bytes]) + body: Future[(Boolean, Bytes)]) { override def toString: String = compound_name(theory_name, name) def write(db: SQL.Database) { - val bytes = body.join + val (compressed, bytes) = body.join db.using_statement(Data.table.insert())(stmt => { stmt.string(1) = session_name @@ -82,8 +81,14 @@ }) } - def body_uncompressed: Bytes = - if (compressed) body.join.uncompress() else body.join + def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes = + { + val (compressed, bytes) = body.join + if (compressed) bytes.uncompress(cache = cache) else bytes + } + + def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body = + YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache))) } def make_regex(pattern: String): Regex = @@ -111,10 +116,12 @@ regex.pattern.matcher(compound_name(theory_name, name)).matches } - def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry = + def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes, + cache: XZ.Cache = XZ.cache()): Entry = { - Entry(session_name, args.theory_name, args.name, args.compress, - if (args.compress) Future.fork(body.compress()) else Future.value(body)) + Entry(session_name, args.theory_name, args.name, + if (args.compress) Future.fork(body.maybe_compress(cache = cache)) + else Future.value((false, body))) } def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry = @@ -128,7 +135,7 @@ if (res.next()) { val compressed = res.bool(Data.compressed) val body = res.bytes(Data.body) - Entry(session_name, theory_name, name, compressed, Future.value(body)) + Entry(session_name, theory_name, name, Future.value(compressed, body)) } else error(message("Bad export", theory_name, name)) }) @@ -141,6 +148,8 @@ class Consumer private[Export](db: SQL.Database) { + val xz_cache = XZ.make_cache() + db.create_table(Data.table) private val export_errors = Synchronized[List[String]](Nil) @@ -160,7 +169,7 @@ }) def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit = - consumer.send(make_entry(session_name, args, body)) + consumer.send(make_entry(session_name, args, body, cache = xz_cache)) def shutdown(close: Boolean = false): List[String] = { @@ -262,6 +271,8 @@ // export if (export_pattern != "") { + val xz_cache = XZ.make_cache() + val matcher = make_matcher(export_pattern) for { (theory_name, name) <- export_names if matcher(theory_name, name) } { @@ -270,7 +281,7 @@ progress.echo("exporting " + path) Isabelle_System.mkdirs(path.dir) - Bytes.write(path, entry.body_uncompressed) + Bytes.write(path, entry.uncompressed(cache = xz_cache)) } } } diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/Thy/export_theory.ML Sun May 13 21:59:41 2018 +0200 @@ -6,56 +6,89 @@ signature EXPORT_THEORY = sig - val export_table_diff: ('a -> XML.tree list option) -> - 'a Name_Space.table list -> 'a Name_Space.table -> XML.tree list + val entity_markup: Name_Space.T -> string -> Markup.T end; structure Export_Theory: EXPORT_THEORY = struct -(* export namespace table *) +(* name space entries *) -fun export_table_diff export_decl prev_tables table = - (table, []) |-> Name_Space.fold_table (fn (name, decl) => - if exists (fn prev => Name_Space.defined prev name) prev_tables then I +fun entity_markup space name = + let + val {serial, pos, ...} = Name_Space.the_entry space name; + val props = Markup.serial_properties serial @ Position.offset_properties_of pos; + in (Markup.entityN, (Markup.nameN, name) :: props) end; + +fun export_decls export_decl parents thy space decls = + (decls, []) |-> fold (fn (name, decl) => + if exists (fn space => Name_Space.declared space name) parents then I else - (case export_decl decl of + (case export_decl thy name decl of NONE => I - | SOME body => - let val markup = Name_Space.markup_def (Name_Space.space_of_table table) name - in cons (name, XML.Elem (markup, body)) end)) + | SOME body => cons (name, XML.Elem (entity_markup space name, body)))) |> sort_by #1 |> map #2; (* present *) -fun present get export name thy = +fun present get_space get_decls export name thy = if Options.default_bool "export_theory" then - (case export (map get (Theory.parents_of thy)) (get thy) of + (case export (map get_space (Theory.parents_of thy)) thy (get_space thy) (get_decls thy) of [] => () | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body]) else (); +fun present_decls get_space get_decls = + present get_space get_decls o export_decls; + +val setup_presentation = Theory.setup o Thy_Info.add_presentation; + (* types *) -val present_types = present (#types o Type.rep_tsig o Sign.tsig_of) o export_table_diff; +local -fun export_logical_type (Type.LogicalType n) = SOME (XML.Encode.int n) - | export_logical_type _ = NONE; +val present_types = + present_decls Sign.type_space (Name_Space.dest_table o #types o Type.rep_tsig o Sign.tsig_of); -fun export_abbreviation (Type.Abbreviation (vs, U, _)) = - let open XML.Encode Term_XML.Encode - in SOME (pair (list string) typ (vs, U)) end - | export_abbreviation _ = NONE; +val encode_type = + let open XML.Encode Term_XML.Encode + in pair (list string) (option typ) end; -fun export_nonterminal Type.Nonterminal = SOME [] - | export_nonterminal _ = NONE; +fun export_type (Type.LogicalType n) = SOME (encode_type (Name.invent Name.context Name.aT n, NONE)) + | export_type (Type.Abbreviation (args, U, false)) = SOME (encode_type (args, SOME U)) + | export_type _ = NONE; -val _ = - Theory.setup - (Thy_Info.add_presentation (present_types export_logical_type "types") #> - Thy_Info.add_presentation (present_types export_abbreviation "type_synonyms") #> - Thy_Info.add_presentation (present_types export_nonterminal "nonterminals")); +in + +val _ = setup_presentation (present_types (K (K export_type)) "types"); end; + + +(* consts *) + +local + +val present_consts = + present_decls Sign.const_space (#constants o Consts.dest o Sign.consts_of); + +val encode_const = + let open XML.Encode Term_XML.Encode + in triple (list string) typ (option term) end; + +fun export_const thy c (T, abbrev) = + let + val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts; + val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts); + val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T')); + in SOME (encode_const (args, T', abbrev')) end; + +in + +val _ = setup_presentation (present_consts export_const "consts"); + +end; + +end; diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/Thy/export_theory.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/export_theory.scala Sun May 13 21:59:41 2018 +0200 @@ -0,0 +1,65 @@ +/* Title: Pure/Thy/export_theory.scala + Author: Makarius + +Export foundational theory content. +*/ + +package isabelle + + +object Export_Theory +{ + /* entities */ + + sealed case class Entity(name: String, serial: Long, pos: Position.T) + { + override def toString: String = name + } + + def decode_entity(tree: XML.Tree): (Entity, XML.Body) = + { + def err(): Nothing = throw new XML.XML_Body(List(tree)) + + tree match { + case XML.Elem(Markup(Markup.ENTITY, props), body) => + val name = Markup.Name.unapply(props) getOrElse err() + val serial = Markup.Serial.unapply(props) getOrElse err() + val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) + (Entity(name, serial, pos), body) + case _ => err() + } + } + + + /* types */ + + sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ]) + + def decode_type(tree: XML.Tree): Type = + { + val (entity, body) = decode_entity(tree) + val (args, abbrev) = + { + import XML.Decode._ + pair(list(string), option(Term_XML.Decode.typ))(body) + } + Type(entity, args, abbrev) + } + + + /* consts */ + + sealed case class Const( + entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term]) + + def decode_const(tree: XML.Tree): Const = + { + val (entity, body) = decode_entity(tree) + val (args, typ, abbrev) = + { + import XML.Decode._ + triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body) + } + Const(entity, args, typ, abbrev) + } +} diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/Thy/sessions.scala Sun May 13 21:59:41 2018 +0200 @@ -973,7 +973,7 @@ /* SQL database content */ - val xml_cache = new XML.Cache() + val xml_cache = XML.make_cache() val xz_cache = XZ.make_cache() def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/Tools/server_commands.scala Sun May 13 21:59:41 2018 +0200 @@ -220,7 +220,7 @@ val matcher = Export.make_matcher(args.export_pattern) for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) } yield { - val (base64, body) = entry.body.join.maybe_base64 + val (base64, body) = entry.uncompressed().maybe_base64 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) } })))) diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/build-jars --- a/src/Pure/build-jars Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/build-jars Sun May 13 21:59:41 2018 +0200 @@ -128,6 +128,7 @@ System/tty_loop.scala Thy/bibtex.scala Thy/export.scala + Thy/export_theory.scala Thy/html.scala Thy/latex.scala Thy/present.scala diff -r 61878d2aa6c7 -r 7c4793e39dd5 src/Pure/theory.ML --- a/src/Pure/theory.ML Sun May 13 14:40:40 2018 +0200 +++ b/src/Pure/theory.ML Sun May 13 21:59:41 2018 +0200 @@ -157,7 +157,7 @@ val axiom_table = #axioms o rep_theory; val axiom_space = Name_Space.space_of_table o axiom_table; -fun axioms_of thy = rev (Name_Space.fold_table cons (axiom_table thy) []); +val axioms_of = Name_Space.dest_table o axiom_table; fun all_axioms_of thy = maps axioms_of (nodes_of thy); val defs_of = #defs o rep_theory;