--- a/src/Pure/ML/ml_heap.scala Mon Jul 10 12:48:26 2023 +0100
+++ b/src/Pure/ML/ml_heap.scala Mon Jul 10 16:56:42 2023 +0200
@@ -66,6 +66,17 @@
val table = make_table(List(name, slice, content), name = "slices")
}
+ object Slices_Size {
+ val name = Generic.name
+ val slice = SQL.Column.int("slice").make_primary_key
+ val size = SQL.Column.long("size")
+
+ val table = make_table(List(name, slice, size),
+ body = "SELECT name, slice, pg_size_pretty(length(content)::bigint) as size FROM " +
+ Slices.table.ident,
+ name = "slices_size")
+ }
+
def get_entry(db: SQL.Database, name: String): Option[SHA1.Digest] =
db.execute_query_statementO[String](
Base.table.select(List(Base.digest), sql = Generic.name.where_equal(name)),
@@ -82,6 +93,7 @@
for (table <- List(Base.table, Slices.table)) {
db.execute_statement(table.delete(sql = Base.name.where_equal(name)))
}
+ db.create_view(Slices_Size.table)
}
def prepare_entry(db: SQL.Database, name: String): Unit =
--- a/src/Pure/PIDE/command.ML Mon Jul 10 12:48:26 2023 +0100
+++ b/src/Pure/PIDE/command.ML Mon Jul 10 16:56:42 2023 +0200
@@ -123,7 +123,12 @@
else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span);
val _ =
if Toplevel.is_ignored tr orelse Toplevel.is_malformed tr then ()
- else Position.report (#1 core_range) (Markup.command_span (Toplevel.name_of tr));
+ else
+ let
+ val name = Toplevel.name_of tr;
+ val kind = the_default "" (Keyword.command_kind (Thy_Header.get_keywords thy) name);
+ val markup = Markup.command_span {name = name, kind = kind};
+ in Position.report (#1 core_range) markup end;
in tr end;
end;
--- a/src/Pure/PIDE/markup.ML Mon Jul 10 12:48:26 2023 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Jul 10 16:56:42 2023 +0200
@@ -172,7 +172,7 @@
val descriptionN: string
val inputN: string val input: bool -> Properties.T -> T
val command_keywordN: string val command_keyword: T
- val command_spanN: string val command_span: string -> T
+ val command_spanN: string val command_span: {name: string, kind: string} -> T
val commandN: string val command_properties: T -> T
val keywordN: string val keyword_properties: T -> T
val stringN: string val string: T
@@ -630,7 +630,11 @@
(* outer syntax *)
val (command_keywordN, command_keyword) = markup_elem "command_keyword";
-val (command_spanN, command_span) = markup_string "command_span" nameN;
+
+val command_spanN = "command_span";
+fun command_span {name, kind} : T =
+ (command_spanN,
+ (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
val commandN = "command"; val command_properties = properties [(kindN, commandN)];
val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
--- a/src/Pure/PIDE/markup.scala Mon Jul 10 12:48:26 2023 +0100
+++ b/src/Pure/PIDE/markup.scala Mon Jul 10 16:56:42 2023 +0200
@@ -420,7 +420,22 @@
/* outer syntax */
val COMMAND_SPAN = "command_span"
- val Command_Span = new Markup_String(COMMAND_SPAN, NAME)
+ object Command_Span {
+ sealed case class Arg(name: String, kind: String) {
+ def properties: Properties.T =
+ (if (name.isEmpty) Nil else Name(name)) :::
+ (if (kind.isEmpty) Nil else Kind(kind))
+ }
+
+ def apply(arg: Arg): Markup = Markup(COMMAND_SPAN, arg.properties)
+ def apply(name: String, kind: String): Markup = apply(Arg(name, kind))
+
+ def unapply(markup: Markup): Option[Arg] =
+ if (markup.name == COMMAND_SPAN) {
+ Some(Arg(Name.get(markup.properties), Kind.get(markup.properties)))
+ }
+ else None
+ }
val COMMAND = "command"
val KEYWORD = "keyword"
--- a/src/Pure/Thy/browser_info.scala Mon Jul 10 12:48:26 2023 +0100
+++ b/src/Pure/Thy/browser_info.scala Mon Jul 10 16:56:42 2023 +0200
@@ -598,7 +598,7 @@
def err(): Nothing =
error("Missing document information for theory: " + quote(theory_name))
- val snapshot = Build_Job.read_theory(session_context.theory(theory_name)) getOrElse err()
+ val snapshot = Build.read_theory(session_context.theory(theory_name)) getOrElse err()
val theory = context.theory_by_name(session_name, theory_name) getOrElse err()
progress.echo("Presenting theory " + quote(theory_name), verbose = true)
--- a/src/Pure/Tools/build.scala Mon Jul 10 12:48:26 2023 +0100
+++ b/src/Pure/Tools/build.scala Mon Jul 10 16:56:42 2023 +0200
@@ -643,7 +643,7 @@
for (thy <- print_theories) {
val thy_heading = "\nTheory " + quote(thy) + " (in " + session_name + ")" + ":"
- Build_Job.read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
+ Build.read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
case None => progress.echo(thy_heading + " MISSING")
case Some(snapshot) =>
val rendering = new Rendering(snapshot, options, session)
--- a/src/Pure/Tools/build_job.scala Mon Jul 10 12:48:26 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Jul 10 16:56:42 2023 +0200
@@ -527,74 +527,4 @@
override def is_finished: Boolean = future_result.is_finished
override def join: (Process_Result, SHA1.Shasum) = future_result.join
}
-
-
- /* theory markup/messages from session database */
-
- def read_theory(
- theory_context: Export.Theory_Context,
- unicode_symbols: Boolean = false
- ): Option[Document.Snapshot] = {
- def decode_bytes(bytes: Bytes): String =
- Symbol.output(unicode_symbols, UTF8.decode_permissive(bytes))
-
- def read(name: String): Export.Entry = theory_context(name, permissive = true)
-
- def read_xml(name: String): XML.Body =
- YXML.parse_body(decode_bytes(read(name).bytes), cache = theory_context.cache)
-
- def read_source_file(name: String): Store.Source_File =
- theory_context.session_context.source_file(name)
-
- for {
- id <- theory_context.document_id()
- (thy_file, blobs_files) <- theory_context.files(permissive = true)
- }
- yield {
- val master_dir =
- Path.explode(Url.strip_base_name(thy_file).getOrElse(
- error("Cannot determine theory master directory: " + quote(thy_file))))
-
- val blobs =
- blobs_files.map { name =>
- val path = Path.explode(name)
- val src_path = File.relative_path(master_dir, path).getOrElse(path)
-
- val file = read_source_file(name)
- val bytes = file.bytes
- val text = decode_bytes(bytes)
- val chunk = Symbol.Text_Chunk(text)
-
- Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) ->
- Document.Blobs.Item(bytes, text, chunk, changed = false)
- }
-
- val thy_source = decode_bytes(read_source_file(thy_file).bytes)
- val thy_xml = read_xml(Export.MARKUP)
- val blobs_xml =
- for (i <- (1 to blobs.length).toList)
- yield read_xml(Export.MARKUP + i)
-
- val markups_index = Command.Markup_Index.make(blobs.map(_._1))
- val markups =
- Command.Markups.make(
- for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
- yield index -> Markup_Tree.from_XML(xml))
-
- val results =
- Command.Results.make(
- for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
- yield i -> elem)
-
- val command =
- Command.unparsed(thy_source, theory = true, id = id,
- node_name = Document.Node.Name(thy_file, theory = theory_context.theory),
- blobs_info = Command.Blobs_Info.make(blobs),
- markups = markups, results = results)
-
- val doc_blobs = Document.Blobs.make(blobs)
-
- Document.State.init.snippet(command, doc_blobs)
- }
- }
}
--- a/src/Pure/Tools/profiling_report.scala Mon Jul 10 12:48:26 2023 +0100
+++ b/src/Pure/Tools/profiling_report.scala Mon Jul 10 16:56:42 2023 +0200
@@ -29,7 +29,7 @@
(for {
thy <- used_theories.iterator
if theories.isEmpty || theories.contains(thy)
- snapshot <- Build_Job.read_theory(session_context.theory(thy)).iterator
+ snapshot <- Build.read_theory(session_context.theory(thy)).iterator
(Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
} yield if (clean_name) report.clean_name else report).toList
--- a/src/Pure/Tools/update.scala Mon Jul 10 12:48:26 2023 +0100
+++ b/src/Pure/Tools/update.scala Mon Jul 10 16:56:42 2023 +0200
@@ -109,7 +109,7 @@
seen_theory += theory
val theory_context = session_context.theory(theory)
for {
- theory_snapshot <- Build_Job.read_theory(theory_context)
+ theory_snapshot <- Build.read_theory(theory_context)
node_name <- theory_snapshot.node_files
snapshot = theory_snapshot.switch(node_name)
if snapshot.node.source_wellformed