merged
authorwenzelm
Sun May 13 21:59:41 2018 +0200 (14 months ago)
changeset 681747c4793e39dd5
parent 68162 61878d2aa6c7
parent 68173 7ed88a534bb6
child 68175 e0bd5089eabf
child 68177 6e40f5d43936
merged
     1.1 --- a/src/Pure/Admin/build_log.scala	Sun May 13 14:40:40 2018 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Sun May 13 21:59:41 2018 +0200
     1.3 @@ -253,7 +253,7 @@
     1.4  
     1.5      /* properties (YXML) */
     1.6  
     1.7 -    val xml_cache = new XML.Cache()
     1.8 +    val xml_cache = XML.make_cache()
     1.9  
    1.10      def parse_props(text: String): Properties.T =
    1.11        try {
    1.12 @@ -881,7 +881,7 @@
    1.13  
    1.14    class Store private[Build_Log](options: Options)
    1.15    {
    1.16 -    val xml_cache: XML.Cache = new XML.Cache()
    1.17 +    val xml_cache: XML.Cache = XML.make_cache()
    1.18      val xz_cache: XZ.Cache = XZ.make_cache()
    1.19  
    1.20      def open_database(
     2.1 --- a/src/Pure/General/bytes.scala	Sun May 13 14:40:40 2018 +0200
     2.2 +++ b/src/Pure/General/bytes.scala	Sun May 13 21:59:41 2018 +0200
     2.3 @@ -205,4 +205,11 @@
     2.4      using(new XZOutputStream(result, options, cache))(write_stream(_))
     2.5      new Bytes(result.toByteArray, 0, result.size)
     2.6    }
     2.7 +
     2.8 +  def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache())
     2.9 +    : (Boolean, Bytes) =
    2.10 +  {
    2.11 +    val compressed = compress(options = options, cache = cache)
    2.12 +    if (compressed.length < length) (true, compressed) else (false, this)
    2.13 +  }
    2.14  }
     3.1 --- a/src/Pure/General/name_space.ML	Sun May 13 14:40:40 2018 +0200
     3.2 +++ b/src/Pure/General/name_space.ML	Sun May 13 21:59:41 2018 +0200
     3.3 @@ -62,6 +62,7 @@
     3.4    val alias: naming -> binding -> string -> T -> T
     3.5    val naming_of: Context.generic -> naming
     3.6    val map_naming: (naming -> naming) -> Context.generic -> Context.generic
     3.7 +  val declared: T -> string -> bool
     3.8    val declare: Context.generic -> bool -> binding -> T -> string * T
     3.9    type 'a table
    3.10    val change_base: bool -> 'a table -> 'a table
    3.11 @@ -80,6 +81,7 @@
    3.12    val del_table: string -> 'a table -> 'a table
    3.13    val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table
    3.14    val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
    3.15 +  val dest_table: 'a table -> (string * 'a) list
    3.16    val empty_table: string -> 'a table
    3.17    val merge_tables: 'a table * 'a table -> 'a table
    3.18    val join_tables: (string -> 'a * 'a -> 'a) (*exception Change_Table.SAME*) ->
    3.19 @@ -503,6 +505,8 @@
    3.20  
    3.21  (* declaration *)
    3.22  
    3.23 +fun declared (Name_Space {entries, ...}) = Change_Table.defined entries;
    3.24 +
    3.25  fun declare context strict binding space =
    3.26    let
    3.27      val naming = naming_of context;
    3.28 @@ -608,6 +612,7 @@
    3.29    Table (space, Change_Table.map_entry name f tab);
    3.30  
    3.31  fun fold_table f (Table (_, tab)) = Change_Table.fold f tab;
    3.32 +fun dest_table (Table (_, tab)) = Change_Table.dest tab;
    3.33  
    3.34  fun empty_table kind = Table (empty kind, Change_Table.empty);
    3.35  
     4.1 --- a/src/Pure/General/position.ML	Sun May 13 14:40:40 2018 +0200
     4.2 +++ b/src/Pure/General/position.ML	Sun May 13 21:59:41 2018 +0200
     4.3 @@ -32,6 +32,7 @@
     4.4    val parse_id: T -> int option
     4.5    val of_properties: Properties.T -> T
     4.6    val properties_of: T -> Properties.T
     4.7 +  val offset_properties_of: T -> Properties.T
     4.8    val def_properties_of: T -> Properties.T
     4.9    val entity_properties_of: bool -> serial -> T -> Properties.T
    4.10    val default_properties: T -> Properties.T -> Properties.T
    4.11 @@ -161,6 +162,9 @@
    4.12  fun properties_of (Pos ((i, j, k), props)) =
    4.13    value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
    4.14  
    4.15 +fun offset_properties_of (Pos ((_, j, k), _)) =
    4.16 +  value Markup.offsetN j @ value Markup.end_offsetN k;
    4.17 +
    4.18  val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
    4.19  
    4.20  fun entity_properties_of def serial pos =
     5.1 --- a/src/Pure/PIDE/session.scala	Sun May 13 14:40:40 2018 +0200
     5.2 +++ b/src/Pure/PIDE/session.scala	Sun May 13 21:59:41 2018 +0200
     5.3 @@ -118,7 +118,8 @@
     5.4  {
     5.5    session =>
     5.6  
     5.7 -  val xml_cache: XML.Cache = new XML.Cache()
     5.8 +  val xml_cache: XML.Cache = XML.make_cache()
     5.9 +  val xz_cache: XZ.Cache = XZ.make_cache()
    5.10  
    5.11  
    5.12    /* global flags */
    5.13 @@ -436,8 +437,8 @@
    5.14                case Markup.Export(args)
    5.15                if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
    5.16                  val id = Value.Long.unapply(args.id.get).get
    5.17 -                val entry = (args.serial, Export.make_entry("", args, msg.bytes))
    5.18 -                change_command(_.add_export(id, entry))
    5.19 +                val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
    5.20 +                change_command(_.add_export(id, (args.serial, export)))
    5.21  
    5.22                case Markup.Assign_Update =>
    5.23                  msg.text match {
     6.1 --- a/src/Pure/PIDE/xml.scala	Sun May 13 14:40:40 2018 +0200
     6.2 +++ b/src/Pure/PIDE/xml.scala	Sun May 13 21:59:41 2018 +0200
     6.3 @@ -154,7 +154,10 @@
     6.4  
     6.5    /** cache for partial sharing (weak table) **/
     6.6  
     6.7 -  class Cache(initial_size: Int = 131071, max_string: Int = 100)
     6.8 +  def make_cache(initial_size: Int = 131071, max_string: Int = 100): Cache =
     6.9 +    new Cache(initial_size, max_string)
    6.10 +
    6.11 +  class Cache private[XML](initial_size: Int, max_string: Int)
    6.12    {
    6.13      private val table =
    6.14        Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
     7.1 --- a/src/Pure/System/isabelle_process.scala	Sun May 13 14:40:40 2018 +0200
     7.2 +++ b/src/Pure/System/isabelle_process.scala	Sun May 13 21:59:41 2018 +0200
     7.3 @@ -42,7 +42,7 @@
     7.4      cwd: JFile = null,
     7.5      env: Map[String, String] = Isabelle_System.settings(),
     7.6      receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
     7.7 -    xml_cache: XML.Cache = new XML.Cache(),
     7.8 +    xml_cache: XML.Cache = XML.make_cache(),
     7.9      sessions: Option[Sessions.Structure] = None,
    7.10      store: Sessions.Store = Sessions.store()): Prover =
    7.11    {
     8.1 --- a/src/Pure/Thy/export.ML	Sun May 13 14:40:40 2018 +0200
     8.2 +++ b/src/Pure/Thy/export.ML	Sun May 13 21:59:41 2018 +0200
     8.3 @@ -33,7 +33,7 @@
     8.4      name = check_name name,
     8.5      compress = compress} body;
     8.6  
     8.7 -fun export thy name body = gen_export (fold (Integer.add o size) body 0 > 60) thy name body;
     8.8 +val export = gen_export true;
     8.9  val export_raw = gen_export false;
    8.10  
    8.11  end;
     9.1 --- a/src/Pure/Thy/export.scala	Sun May 13 14:40:40 2018 +0200
     9.2 +++ b/src/Pure/Thy/export.scala	Sun May 13 21:59:41 2018 +0200
     9.3 @@ -63,14 +63,13 @@
     9.4      session_name: String,
     9.5      theory_name: String,
     9.6      name: String,
     9.7 -    compressed: Boolean,
     9.8 -    body: Future[Bytes])
     9.9 +    body: Future[(Boolean, Bytes)])
    9.10    {
    9.11      override def toString: String = compound_name(theory_name, name)
    9.12  
    9.13      def write(db: SQL.Database)
    9.14      {
    9.15 -      val bytes = body.join
    9.16 +      val (compressed, bytes) = body.join
    9.17        db.using_statement(Data.table.insert())(stmt =>
    9.18        {
    9.19          stmt.string(1) = session_name
    9.20 @@ -82,8 +81,14 @@
    9.21        })
    9.22      }
    9.23  
    9.24 -    def body_uncompressed: Bytes =
    9.25 -      if (compressed) body.join.uncompress() else body.join
    9.26 +    def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
    9.27 +    {
    9.28 +      val (compressed, bytes) = body.join
    9.29 +      if (compressed) bytes.uncompress(cache = cache) else bytes
    9.30 +    }
    9.31 +
    9.32 +    def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body =
    9.33 +      YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache)))
    9.34    }
    9.35  
    9.36    def make_regex(pattern: String): Regex =
    9.37 @@ -111,10 +116,12 @@
    9.38        regex.pattern.matcher(compound_name(theory_name, name)).matches
    9.39    }
    9.40  
    9.41 -  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry =
    9.42 +  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
    9.43 +    cache: XZ.Cache = XZ.cache()): Entry =
    9.44    {
    9.45 -    Entry(session_name, args.theory_name, args.name, args.compress,
    9.46 -      if (args.compress) Future.fork(body.compress()) else Future.value(body))
    9.47 +    Entry(session_name, args.theory_name, args.name,
    9.48 +      if (args.compress) Future.fork(body.maybe_compress(cache = cache))
    9.49 +      else Future.value((false, body)))
    9.50    }
    9.51  
    9.52    def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
    9.53 @@ -128,7 +135,7 @@
    9.54        if (res.next()) {
    9.55          val compressed = res.bool(Data.compressed)
    9.56          val body = res.bytes(Data.body)
    9.57 -        Entry(session_name, theory_name, name, compressed, Future.value(body))
    9.58 +        Entry(session_name, theory_name, name, Future.value(compressed, body))
    9.59        }
    9.60        else error(message("Bad export", theory_name, name))
    9.61      })
    9.62 @@ -141,6 +148,8 @@
    9.63  
    9.64    class Consumer private[Export](db: SQL.Database)
    9.65    {
    9.66 +    val xz_cache = XZ.make_cache()
    9.67 +
    9.68      db.create_table(Data.table)
    9.69  
    9.70      private val export_errors = Synchronized[List[String]](Nil)
    9.71 @@ -160,7 +169,7 @@
    9.72          })
    9.73  
    9.74      def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
    9.75 -      consumer.send(make_entry(session_name, args, body))
    9.76 +      consumer.send(make_entry(session_name, args, body, cache = xz_cache))
    9.77  
    9.78      def shutdown(close: Boolean = false): List[String] =
    9.79      {
    9.80 @@ -262,6 +271,8 @@
    9.81  
    9.82          // export
    9.83          if (export_pattern != "") {
    9.84 +          val xz_cache = XZ.make_cache()
    9.85 +
    9.86            val matcher = make_matcher(export_pattern)
    9.87            for { (theory_name, name) <- export_names if matcher(theory_name, name) }
    9.88            {
    9.89 @@ -270,7 +281,7 @@
    9.90  
    9.91              progress.echo("exporting " + path)
    9.92              Isabelle_System.mkdirs(path.dir)
    9.93 -            Bytes.write(path, entry.body_uncompressed)
    9.94 +            Bytes.write(path, entry.uncompressed(cache = xz_cache))
    9.95            }
    9.96          }
    9.97        }
    10.1 --- a/src/Pure/Thy/export_theory.ML	Sun May 13 14:40:40 2018 +0200
    10.2 +++ b/src/Pure/Thy/export_theory.ML	Sun May 13 21:59:41 2018 +0200
    10.3 @@ -6,56 +6,89 @@
    10.4  
    10.5  signature EXPORT_THEORY =
    10.6  sig
    10.7 -  val export_table_diff: ('a -> XML.tree list option) ->
    10.8 -    'a Name_Space.table list -> 'a Name_Space.table -> XML.tree list
    10.9 +  val entity_markup: Name_Space.T -> string -> Markup.T
   10.10  end;
   10.11  
   10.12  structure Export_Theory: EXPORT_THEORY =
   10.13  struct
   10.14  
   10.15 -(* export namespace table *)
   10.16 +(* name space entries *)
   10.17  
   10.18 -fun export_table_diff export_decl prev_tables table =
   10.19 -  (table, []) |-> Name_Space.fold_table (fn (name, decl) =>
   10.20 -    if exists (fn prev => Name_Space.defined prev name) prev_tables then I
   10.21 +fun entity_markup space name =
   10.22 +  let
   10.23 +    val {serial, pos, ...} = Name_Space.the_entry space name;
   10.24 +    val props = Markup.serial_properties serial @ Position.offset_properties_of pos;
   10.25 +  in (Markup.entityN, (Markup.nameN, name) :: props) end;
   10.26 +
   10.27 +fun export_decls export_decl parents thy space decls =
   10.28 +  (decls, []) |-> fold (fn (name, decl) =>
   10.29 +    if exists (fn space => Name_Space.declared space name) parents then I
   10.30      else
   10.31 -      (case export_decl decl of
   10.32 +      (case export_decl thy name decl of
   10.33          NONE => I
   10.34 -      | SOME body =>
   10.35 -          let val markup = Name_Space.markup_def (Name_Space.space_of_table table) name
   10.36 -          in cons (name, XML.Elem (markup, body)) end))
   10.37 +      | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
   10.38    |> sort_by #1 |> map #2;
   10.39  
   10.40  
   10.41  (* present *)
   10.42  
   10.43 -fun present get export name thy =
   10.44 +fun present get_space get_decls export name thy =
   10.45    if Options.default_bool "export_theory" then
   10.46 -    (case export (map get (Theory.parents_of thy)) (get thy) of
   10.47 +    (case export (map get_space (Theory.parents_of thy)) thy (get_space thy) (get_decls thy) of
   10.48        [] => ()
   10.49      | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body])
   10.50    else ();
   10.51  
   10.52 +fun present_decls get_space get_decls =
   10.53 +  present get_space get_decls o export_decls;
   10.54 +
   10.55 +val setup_presentation = Theory.setup o Thy_Info.add_presentation;
   10.56 +
   10.57  
   10.58  (* types *)
   10.59  
   10.60 -val present_types = present (#types o Type.rep_tsig o Sign.tsig_of) o export_table_diff;
   10.61 +local
   10.62  
   10.63 -fun export_logical_type (Type.LogicalType n) = SOME (XML.Encode.int n)
   10.64 -  | export_logical_type _ = NONE;
   10.65 +val present_types =
   10.66 +  present_decls Sign.type_space (Name_Space.dest_table o #types o Type.rep_tsig o Sign.tsig_of);
   10.67  
   10.68 -fun export_abbreviation (Type.Abbreviation (vs, U, _)) =
   10.69 -      let open XML.Encode Term_XML.Encode
   10.70 -      in SOME (pair (list string) typ (vs, U)) end
   10.71 -  | export_abbreviation _ = NONE;
   10.72 +val encode_type =
   10.73 +  let open XML.Encode Term_XML.Encode
   10.74 +  in pair (list string) (option typ) end;
   10.75  
   10.76 -fun export_nonterminal Type.Nonterminal = SOME []
   10.77 -  | export_nonterminal _ = NONE;
   10.78 +fun export_type (Type.LogicalType n) = SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
   10.79 +  | export_type (Type.Abbreviation (args, U, false)) = SOME (encode_type (args, SOME U))
   10.80 +  | export_type _ = NONE;
   10.81  
   10.82 -val _ =
   10.83 -  Theory.setup
   10.84 -    (Thy_Info.add_presentation (present_types export_logical_type "types") #>
   10.85 -     Thy_Info.add_presentation (present_types export_abbreviation "type_synonyms") #>
   10.86 -     Thy_Info.add_presentation (present_types export_nonterminal "nonterminals"));
   10.87 +in
   10.88 +
   10.89 +val _ = setup_presentation (present_types (K (K export_type)) "types");
   10.90  
   10.91  end;
   10.92 +
   10.93 +
   10.94 +(* consts *)
   10.95 +
   10.96 +local
   10.97 +
   10.98 +val present_consts =
   10.99 +  present_decls Sign.const_space (#constants o Consts.dest o Sign.consts_of);
  10.100 +
  10.101 +val encode_const =
  10.102 +  let open XML.Encode Term_XML.Encode
  10.103 +  in triple (list string) typ (option term) end;
  10.104 +
  10.105 +fun export_const thy c (T, abbrev) =
  10.106 +  let
  10.107 +    val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
  10.108 +    val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
  10.109 +    val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
  10.110 +  in SOME (encode_const (args, T', abbrev')) end;
  10.111 +
  10.112 +in
  10.113 +
  10.114 +val _ = setup_presentation (present_consts export_const "consts");
  10.115 +
  10.116 +end;
  10.117 +
  10.118 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/Thy/export_theory.scala	Sun May 13 21:59:41 2018 +0200
    11.3 @@ -0,0 +1,65 @@
    11.4 +/*  Title:      Pure/Thy/export_theory.scala
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Export foundational theory content.
    11.8 +*/
    11.9 +
   11.10 +package isabelle
   11.11 +
   11.12 +
   11.13 +object Export_Theory
   11.14 +{
   11.15 +  /* entities */
   11.16 +
   11.17 +  sealed case class Entity(name: String, serial: Long, pos: Position.T)
   11.18 +  {
   11.19 +    override def toString: String = name
   11.20 +  }
   11.21 +
   11.22 +  def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
   11.23 +  {
   11.24 +    def err(): Nothing = throw new XML.XML_Body(List(tree))
   11.25 +
   11.26 +    tree match {
   11.27 +      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
   11.28 +        val name = Markup.Name.unapply(props) getOrElse err()
   11.29 +        val serial = Markup.Serial.unapply(props) getOrElse err()
   11.30 +        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
   11.31 +        (Entity(name, serial, pos), body)
   11.32 +      case _ => err()
   11.33 +    }
   11.34 +  }
   11.35 +
   11.36 +
   11.37 +  /* types */
   11.38 +
   11.39 +  sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
   11.40 +
   11.41 +  def decode_type(tree: XML.Tree): Type =
   11.42 +  {
   11.43 +    val (entity, body) = decode_entity(tree)
   11.44 +    val (args, abbrev) =
   11.45 +    {
   11.46 +      import XML.Decode._
   11.47 +      pair(list(string), option(Term_XML.Decode.typ))(body)
   11.48 +    }
   11.49 +    Type(entity, args, abbrev)
   11.50 +  }
   11.51 +
   11.52 +
   11.53 +  /* consts */
   11.54 +
   11.55 +  sealed case class Const(
   11.56 +    entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
   11.57 +
   11.58 +  def decode_const(tree: XML.Tree): Const =
   11.59 +  {
   11.60 +    val (entity, body) = decode_entity(tree)
   11.61 +    val (args, typ, abbrev) =
   11.62 +    {
   11.63 +      import XML.Decode._
   11.64 +      triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   11.65 +    }
   11.66 +    Const(entity, args, typ, abbrev)
   11.67 +  }
   11.68 +}
    12.1 --- a/src/Pure/Thy/sessions.scala	Sun May 13 14:40:40 2018 +0200
    12.2 +++ b/src/Pure/Thy/sessions.scala	Sun May 13 21:59:41 2018 +0200
    12.3 @@ -973,7 +973,7 @@
    12.4  
    12.5      /* SQL database content */
    12.6  
    12.7 -    val xml_cache = new XML.Cache()
    12.8 +    val xml_cache = XML.make_cache()
    12.9      val xz_cache = XZ.make_cache()
   12.10  
   12.11      def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
    13.1 --- a/src/Pure/Tools/server_commands.scala	Sun May 13 14:40:40 2018 +0200
    13.2 +++ b/src/Pure/Tools/server_commands.scala	Sun May 13 21:59:41 2018 +0200
    13.3 @@ -220,7 +220,7 @@
    13.4                      val matcher = Export.make_matcher(args.export_pattern)
    13.5                      for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) }
    13.6                      yield {
    13.7 -                      val (base64, body) = entry.body.join.maybe_base64
    13.8 +                      val (base64, body) = entry.uncompressed().maybe_base64
    13.9                        JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
   13.10                      }
   13.11                    }))))
    14.1 --- a/src/Pure/build-jars	Sun May 13 14:40:40 2018 +0200
    14.2 +++ b/src/Pure/build-jars	Sun May 13 21:59:41 2018 +0200
    14.3 @@ -128,6 +128,7 @@
    14.4    System/tty_loop.scala
    14.5    Thy/bibtex.scala
    14.6    Thy/export.scala
    14.7 +  Thy/export_theory.scala
    14.8    Thy/html.scala
    14.9    Thy/latex.scala
   14.10    Thy/present.scala
    15.1 --- a/src/Pure/theory.ML	Sun May 13 14:40:40 2018 +0200
    15.2 +++ b/src/Pure/theory.ML	Sun May 13 21:59:41 2018 +0200
    15.3 @@ -157,7 +157,7 @@
    15.4  val axiom_table = #axioms o rep_theory;
    15.5  val axiom_space = Name_Space.space_of_table o axiom_table;
    15.6  
    15.7 -fun axioms_of thy = rev (Name_Space.fold_table cons (axiom_table thy) []);
    15.8 +val axioms_of = Name_Space.dest_table o axiom_table;
    15.9  fun all_axioms_of thy = maps axioms_of (nodes_of thy);
   15.10  
   15.11  val defs_of = #defs o rep_theory;