# HG changeset patch # User wenzelm # Date 1688999418 -7200 # Node ID 46805acae10c4dbe32a6db07ea1d57881365cf80 # Parent aabbf14723fc5bb4a7076f7457cb3ee573e48fd9# Parent 865b44cbaad17be4e2383dd1d3f07ac09aaf23d7 merged diff -r aabbf14723fc -r 46805acae10c src/Pure/ML/ml_heap.scala --- a/src/Pure/ML/ml_heap.scala Mon Jul 10 10:35:38 2023 +0100 +++ b/src/Pure/ML/ml_heap.scala Mon Jul 10 16:30:18 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 = diff -r aabbf14723fc -r 46805acae10c src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Mon Jul 10 10:35:38 2023 +0100 +++ b/src/Pure/PIDE/command.ML Mon Jul 10 16:30:18 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; diff -r aabbf14723fc -r 46805acae10c src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Mon Jul 10 10:35:38 2023 +0100 +++ b/src/Pure/PIDE/markup.ML Mon Jul 10 16:30:18 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)]; diff -r aabbf14723fc -r 46805acae10c src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Mon Jul 10 10:35:38 2023 +0100 +++ b/src/Pure/PIDE/markup.scala Mon Jul 10 16:30:18 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" diff -r aabbf14723fc -r 46805acae10c src/Pure/Thy/browser_info.scala --- a/src/Pure/Thy/browser_info.scala Mon Jul 10 10:35:38 2023 +0100 +++ b/src/Pure/Thy/browser_info.scala Mon Jul 10 16:30:18 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) diff -r aabbf14723fc -r 46805acae10c src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Jul 10 10:35:38 2023 +0100 +++ b/src/Pure/Tools/build.scala Mon Jul 10 16:30:18 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) diff -r aabbf14723fc -r 46805acae10c src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Mon Jul 10 10:35:38 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Mon Jul 10 16:30:18 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) - } - } } diff -r aabbf14723fc -r 46805acae10c src/Pure/Tools/profiling_report.scala --- a/src/Pure/Tools/profiling_report.scala Mon Jul 10 10:35:38 2023 +0100 +++ b/src/Pure/Tools/profiling_report.scala Mon Jul 10 16:30:18 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 diff -r aabbf14723fc -r 46805acae10c src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Mon Jul 10 10:35:38 2023 +0100 +++ b/src/Pure/Tools/update.scala Mon Jul 10 16:30:18 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