--- 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(
--- 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)
+ }
}
--- 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);
--- 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 =
--- 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 {
--- 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))
--- 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 =
{
--- 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;
--- 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))
}
}
}
--- 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;
--- /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)
+ }
+}
--- 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 =
--- 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)
}
}))))
--- 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
--- 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;