# HG changeset patch # User paulson # Date 1606414155 0 # Node ID 7553c18808158682ea5639b3aada19dba066d674 # Parent 178de0e275a12252e2d5fee87b3cedd6b453ad7f# Parent bbe5d3ef20524868f29552b896ff1b15607bf372 merged diff -r bbe5d3ef2052 -r 7553c1880815 NEWS --- a/NEWS Thu Nov 26 18:09:02 2020 +0000 +++ b/NEWS Thu Nov 26 18:09:15 2020 +0000 @@ -242,6 +242,9 @@ ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g" +This includes full PIDE markup, if option "build_pide_reports" is +enabled. + * The command-line tool "isabelle build" provides option -P DIR to produce PDF/HTML presentation in the specified directory; -P: refers to the standard directory according to ISABELLE_BROWSER_INFO / diff -r bbe5d3ef2052 -r 7553c1880815 etc/options --- a/etc/options Thu Nov 26 18:09:02 2020 +0000 +++ b/etc/options Thu Nov 26 18:09:15 2020 +0000 @@ -150,6 +150,9 @@ option pide_reports : bool = true -- "report PIDE markup" +option build_pide_reports : bool = false + -- "report PIDE markup in batch build" + section "Editor Session" diff -r bbe5d3ef2052 -r 7553c1880815 src/HOL/Data_Structures/Binomial_Heap.thy --- a/src/HOL/Data_Structures/Binomial_Heap.thy Thu Nov 26 18:09:02 2020 +0000 +++ b/src/HOL/Data_Structures/Binomial_Heap.thy Thu Nov 26 18:09:15 2020 +0000 @@ -110,7 +110,7 @@ using assms by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp -lemma invar_link_otree: +lemma invar_otree_link: assumes "invar_otree t\<^sub>1" assumes "invar_otree t\<^sub>2" shows "invar_otree (link t\<^sub>1 t\<^sub>2)" @@ -152,7 +152,7 @@ assumes "invar_oheap ts" shows "invar_oheap (ins_tree t ts)" using assms -by (induction t ts rule: ins_tree.induct) (auto simp: invar_link_otree) +by (induction t ts rule: ins_tree.induct) (auto simp: invar_otree_link) lemma mset_heap_ins_tree[simp]: "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts" @@ -252,7 +252,7 @@ shows "invar_oheap (merge ts\<^sub>1 ts\<^sub>2)" using assms by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) - (auto simp: invar_oheap_ins_tree invar_link_otree) + (auto simp: invar_oheap_ins_tree invar_otree_link) lemma invar_merge[simp]: "\ invar ts\<^sub>1; invar ts\<^sub>2 \ \ invar (merge ts\<^sub>1 ts\<^sub>2)" by (auto simp: invar_def invar_bheap_merge invar_oheap_merge) diff -r bbe5d3ef2052 -r 7553c1880815 src/HOL/Data_Structures/Heaps.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Data_Structures/Heaps.thy Thu Nov 26 18:09:15 2020 +0000 @@ -0,0 +1,87 @@ +(* Author: Tobias Nipkow *) + +section \Heaps\ + +theory Heaps +imports + "HOL-Library.Tree_Multiset" + Priority_Queue_Specs +begin + +text \Heap = priority queue on trees:\ + +locale Heap = +fixes insert :: "('a::linorder) \ 'a tree \ 'a tree" +and del_min :: "'a tree \ 'a tree" +assumes mset_insert: "heap q \ mset_tree (insert x q) = {#x#} + mset_tree q" +and mset_del_min: "\ heap q; q \ Leaf \ \ mset_tree (del_min q) = mset_tree q - {#value q#}" +and heap_insert: "heap q \ heap(insert x q)" +and heap_del_min: "heap q \ heap(del_min q)" +begin + +definition empty :: "'a tree" where +"empty = Leaf" + +fun is_empty :: "'a tree \ bool" where +"is_empty t = (t = Leaf)" + +sublocale Priority_Queue where empty = empty and is_empty = is_empty and insert = insert +and get_min = "value" and del_min = del_min and invar = heap and mset = mset_tree +proof (standard, goal_cases) + case 1 thus ?case by (simp add: empty_def) +next + case 2 thus ?case by(auto) +next + case 3 thus ?case by(simp add: mset_insert) +next + case 4 thus ?case by(simp add: mset_del_min) +next + case 5 thus ?case by(auto simp: neq_Leaf_iff Min_insert2 simp del: Un_iff) +next + case 6 thus ?case by(simp add: empty_def) +next + case 7 thus ?case by(simp add: heap_insert) +next + case 8 thus ?case by(simp add: heap_del_min) +qed + +end + + +text \Once you have \merge\, \insert\ and \del_min\ are easy:\ + +locale Heap_Merge = +fixes merge :: "'a::linorder tree \ 'a tree \ 'a tree" +assumes mset_merge: "\ heap q1; heap q2 \ \ mset_tree (merge q1 q2) = mset_tree q1 + mset_tree q2" +and invar_merge: "\ heap q1; heap q2 \ \ heap (merge q1 q2)" +begin + +fun insert :: "'a \ 'a tree \ 'a tree" where +"insert x t = merge (Node Leaf x Leaf) t" + +fun del_min :: "'a tree \ 'a tree" where +"del_min Leaf = Leaf" | +"del_min (Node l x r) = merge l r" + +interpretation Heap insert del_min +proof(standard, goal_cases) + case 1 thus ?case by(simp add:mset_merge) +next + case (2 q) thus ?case by(cases q)(auto simp: mset_merge) +next + case 3 thus ?case by (simp add: invar_merge) +next + case (4 q) thus ?case by (cases q)(auto simp: invar_merge) +qed + +sublocale PQM: Priority_Queue_Merge where empty = empty and is_empty = is_empty and insert = insert +and get_min = "value" and del_min = del_min and invar = heap and mset = mset_tree and merge = merge +proof(standard, goal_cases) + case 1 thus ?case by (simp add: mset_merge) +next + case 2 thus ?case by (simp add: invar_merge) +qed + +end + +end diff -r bbe5d3ef2052 -r 7553c1880815 src/HOL/ROOT --- a/src/HOL/ROOT Thu Nov 26 18:09:02 2020 +0000 +++ b/src/HOL/ROOT Thu Nov 26 18:09:15 2020 +0000 @@ -285,6 +285,7 @@ Trie_Map Tries_Binary Queue_2Lists + Heaps Leftist_Heap Binomial_Heap document_files "root.tex" "root.bib" diff -r bbe5d3ef2052 -r 7553c1880815 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Nov 26 18:09:02 2020 +0000 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Nov 26 18:09:15 2020 +0000 @@ -561,7 +561,8 @@ (((num, map fst (find_formula_in_problem phi problem)), phi), "", []) else (((num, [s]), phi), "", []) - | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)) + | Inference_Source (rule, deps) => (((num, []), phi), rule, deps) + | Introduced_Source rule => (((num, []), phi), rule, [])) in [(name, role', phi, rule, map (rpair []) deps)] end) diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Admin/build_log.scala Thu Nov 26 18:09:15 2020 +0000 @@ -485,12 +485,10 @@ val Session_Finished1 = new Regex("""^Finished (\S+) $(\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""") val Session_Finished2 = - new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""") + new Regex("""^Finished ([^\s/]+) \((\d+):(\d+):(\d+) elapsed time.*$""") val Session_Timing = new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""") val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""") - val Session_Failed = new Regex("""^(\S+) FAILED""") - val Session_Cancelled = new Regex("""^(\S+) CANCELLED""") val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""") val Heap = new Regex("""^Heap (\S+) \((\d+) bytes$$""") @@ -514,8 +512,6 @@ var timing = Map.empty[String, Timing] var ml_timing = Map.empty[String, Timing] var started = Set.empty[String] - var failed = Set.empty[String] - var cancelled = Set.empty[String] var sources = Map.empty[String, String] var heap_sizes = Map.empty[String, Long] var theory_timings = Map.empty[String, Map[String, Timing]] @@ -524,7 +520,7 @@ def all_sessions: Set[String] = chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++ - failed ++ cancelled ++ started ++ sources.keySet ++ heap_sizes.keySet ++ + started ++ sources.keySet ++ heap_sizes.keySet ++ theory_timings.keySet ++ ml_statistics.keySet @@ -596,9 +592,7 @@ Map( (for (name <- all_sessions.toList) yield { val status = - if (failed(name)) Session_Status.failed - else if (cancelled(name)) Session_Status.cancelled - else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name)) + if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name)) Session_Status.finished else if (started(name)) Session_Status.failed else Session_Status.existing diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/General/file.scala Thu Nov 26 18:09:15 2020 +0000 @@ -222,7 +222,7 @@ val line = try { reader.readLine} catch { case _: IOException => null } - Option(line) + Option(line).map(Library.trim_line) } def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/General/position.ML Thu Nov 26 18:09:15 2020 +0000 @@ -40,7 +40,6 @@ val def_properties_of: T -> Properties.T val entity_markup: string -> string * T -> Markup.T val entity_properties_of: bool -> serial -> T -> Properties.T - val default_properties: T -> Properties.T -> Properties.T val markup: T -> Markup.T -> Markup.T val is_reported: T -> bool val is_reported_range: T -> bool @@ -91,7 +90,7 @@ fun norm_props (props: Properties.T) = maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) - Markup.position_properties'; + [Markup.fileN, Markup.idN]; fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props); fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props}; @@ -211,10 +210,6 @@ if def then (Markup.defN, Value.print_int serial) :: properties_of pos else (Markup.refN, Value.print_int serial) :: def_properties_of pos; -fun default_properties default props = - if exists (member (op =) Markup.position_properties o #1) props then props - else properties_of default @ props; - val markup = Markup.properties o properties_of; diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/General/position.scala Thu Nov 26 18:09:15 2020 +0000 @@ -112,29 +112,12 @@ } } - object Identified - { - def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] = - pos match { - case Id(id) => - val chunk_name = - pos match { - case File(name) => Symbol.Text_Chunk.File(name) - case _ => Symbol.Text_Chunk.Default - } - Some((id, chunk_name)) - case _ => None - } - } - - def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) - /* here: user output */ def here(props: T, delimited: Boolean = true): String = { - val pos = props.filter(p => Markup.POSITION_PROPERTIES(p._1)) + val pos = props.filter(Markup.position_property) if (pos.isEmpty) "" else { val s0 = diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/PIDE/command.scala Thu Nov 26 18:09:15 2020 +0000 @@ -142,7 +142,7 @@ Markup_Index(status, chunk_name) } - (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _) + (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML))(body))(_ + _) } } @@ -331,55 +331,56 @@ xml_cache: XML.Cache): State = message match { case XML.Elem(Markup(Markup.STATUS, _), msgs) => - (this /: msgs)((state, msg) => - msg match { - case elem @ XML.Elem(markup, Nil) => - state. - add_status(markup). - add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) - case _ => - Output.warning("Ignored status message: " + msg) - state - }) + if (command.span.is_theory) this + else { + (this /: msgs)((state, msg) => + msg match { + case elem @ XML.Elem(markup, Nil) => + state. + add_status(markup). + add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) + case _ => + Output.warning("Ignored status message: " + msg) + state + }) + } - case XML.Elem(Markup(Markup.REPORT, _), msgs) => + case XML.Elem(Markup(Markup.REPORT, atts0), msgs) => (this /: msgs)((state, msg) => { def bad(): Unit = Output.warning("Ignored report message: " + msg) msg match { - case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) => - - val target = - if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) - Some((chunk_name, command.chunks(chunk_name))) - else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id) - else None + case XML.Elem(Markup(name, atts1), args) => + val atts = atts1 ::: atts0 + command.reported_position(atts) match { + case Some((id, chunk_name)) => + val target = + if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) + Some((chunk_name, command.chunks(chunk_name))) + else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id) + else None - (target, atts) match { - case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => - target_chunk.incorporate(symbol_range) match { - case Some(range) => - val props = Position.purge(atts) - val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) - state.add_markup(false, target_name, Text.Info(range, elem)) - case None => bad(); state + (target, atts) match { + case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => + target_chunk.incorporate(symbol_range) match { + case Some(range) => + val props = atts.filterNot(Markup.position_property) + val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) + state.add_markup(false, target_name, Text.Info(range, elem)) + case None => bad(); state + } + case _ => + // silently ignore excessive reports + state } - case _ => - // silently ignore excessive reports - state + + case _ => bad(); state } - - case XML.Elem(Markup(name, atts), args) - if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => - val range = command.core_range - val props = Position.purge(atts) - val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) - state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem)) - case _ => bad(); state } }) + case XML.Elem(Markup(name, props), body) => props match { case Markup.Serial(i) => @@ -392,8 +393,7 @@ if (Protocol.is_inlined(message)) { for { (chunk_name, chunk) <- command.chunks.iterator - range <- Protocol_Message.positions( - self_id, command.span.position, chunk_name, chunk, message) + range <- command.message_positions(self_id, chunk_name, chunk, message) } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup)) } st @@ -418,31 +418,29 @@ span: Command_Span.Span): Command = { val (source, span1) = span.compact_source - new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty) + new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty) } val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty) def unparsed( - id: Document_ID.Command, source: String, - results: Results, - markup: Markup_Tree): Command = + theory: Boolean = false, + id: Document_ID.Command = Document_ID.none, + node_name: Document.Node.Name = Document.Node.Name.empty, + results: Results = Results.empty, + markups: Markups = Markups.empty): Command = { - val (source1, span1) = Command_Span.unparsed(source).compact_source - new Command(id, Document.Node.Name.empty, no_blobs, span1, source1, results, markup) + val (source1, span1) = Command_Span.unparsed(source, theory).compact_source + new Command(id, node_name, no_blobs, span1, source1, results, markups) } - def text(source: String): Command = - unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty) + def text(source: String): Command = unparsed(source) def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = - { - val text = XML.content(body) - val markup = Markup_Tree.from_XML(body) - unparsed(id, text, results, markup) - } + unparsed(XML.content(body), id = id, results = results, + markups = Markups.init(Markup_Tree.from_XML(body))) /* perspective */ @@ -557,7 +555,7 @@ val span: Command_Span.Span, val source: String, val init_results: Command.Results, - val init_markup: Markup_Tree) + val init_markups: Command.Markups) { override def toString: String = id + "/" + span.kind.toString @@ -614,10 +612,65 @@ def source(range: Text.Range): String = range.substring(source) + /* reported positions */ + + def reported_position(pos: Position.T): Option[(Document_ID.Generic, Symbol.Text_Chunk.Name)] = + pos match { + case Position.Id(id) => + val chunk_name = + pos match { + case Position.File(name) if name != node_name.node => + Symbol.Text_Chunk.File(name) + case _ => Symbol.Text_Chunk.Default + } + Some((id, chunk_name)) + case _ => None + } + + def message_positions( + self_id: Document_ID.Generic => Boolean, + chunk_name: Symbol.Text_Chunk.Name, + chunk: Symbol.Text_Chunk, + message: XML.Elem): Set[Text.Range] = + { + def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = + reported_position(props) match { + case Some((id, name)) if self_id(id) && name == chunk_name => + val opt_range = + Position.Range.unapply(props) orElse { + if (name == Symbol.Text_Chunk.Default) + Position.Range.unapply(span.position) + else None + } + opt_range match { + case Some(symbol_range) => + chunk.incorporate(symbol_range) match { + case Some(range) => set + range + case _ => set + } + case None => set + } + case _ => set + } + def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] = + t match { + case XML.Wrapped_Elem(Markup(name, props), _, body) => + body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) + case XML.Elem(Markup(name, props), body) => + body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) + case XML.Text(_) => set + } + + val set = tree(Set.empty, message) + if (set.isEmpty) elem(message.markup.properties, set) + else set + } + + /* accumulated results */ val init_state: Command.State = - Command.State(this, results = init_results, markups = Command.Markups.init(init_markup)) + Command.State(this, results = init_results, markups = init_markups) val empty_state: Command.State = Command.State(this) } diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/PIDE/command_span.scala --- a/src/Pure/PIDE/command_span.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/PIDE/command_span.scala Thu Nov 26 18:09:15 2020 +0000 @@ -18,14 +18,18 @@ case Command_Span(name, _) => proper_string(name) getOrElse "" case Ignored_Span => "" case Malformed_Span => "" + case Theory_Span => "" } } case class Command_Span(name: String, pos: Position.T) extends Kind case object Ignored_Span extends Kind case object Malformed_Span extends Kind + case object Theory_Span extends Kind sealed case class Span(kind: Kind, content: List[Token]) { + def is_theory: Boolean = kind == Theory_Span + def name: String = kind match { case Command_Span(name, _) => name case _ => "" } @@ -67,8 +71,11 @@ val empty: Span = Span(Ignored_Span, Nil) - def unparsed(source: String): Span = - Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source))) + def unparsed(source: String, theory: Boolean): Span = + { + val kind = if (theory) Theory_Span else Malformed_Span + Span(kind, List(Token(Token.Kind.UNPARSED, source))) + } /* XML data representation */ diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/PIDE/document.scala Thu Nov 26 18:09:15 2020 +0000 @@ -552,7 +552,29 @@ def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] - def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body + def command_snippet(command: Command): Snapshot = + { + val node_name = command.node_name + + val nodes0 = version.nodes + val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) + val version1 = Document.Version.make(nodes1) + + val edits: List[Edit_Text] = + List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) + + val state0 = state.define_command(command) + val state1 = + state0.continue_history(Future.value(version), edits, Future.value(version1)) + .define_version(version1, state0.the_assignment(version)) + .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2 + + state1.snapshot(name = node_name) + } + + def xml_markup( + range: Text.Range = Text.Range.full, + elements: Markup.Elements = Markup.Elements.full): XML.Body def messages: List[(XML.Tree, Position.T)] def exports: List[Export.Entry] def exports_map: Map[String, Export.Entry] @@ -672,6 +694,8 @@ versions: Map[Document_ID.Version, Version] = Map.empty, /*inlined auxiliary files*/ blobs: Set[SHA1.Digest] = Set.empty, + /*loaded theories in batch builds*/ + theories: Map[Document_ID.Exec, Command.State] = Map.empty, /*static markup from define_command*/ commands: Map[Document_ID.Command, Command.State] = Map.empty, /*dynamic markup from execution*/ @@ -710,7 +734,8 @@ def define_command(command: Command): State = { val id = command.id - copy(commands = commands + (id -> command.init_state)) + if (commands.isDefinedAt(id)) fail + else copy(commands = commands + (id -> command.init_state)) } def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id) @@ -721,7 +746,7 @@ def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail) def lookup_id(id: Document_ID.Generic): Option[Command.State] = - commands.get(id) orElse execs.get(id) + theories.get(id) orElse commands.get(id) orElse execs.get(id) private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean = id == st.command.id || @@ -738,18 +763,21 @@ def accumulate(id: Document_ID.Generic, message: XML.Elem, xml_cache: XML.Cache) : (Command.State, State) = { - execs.get(id) match { - case Some(st) => - val new_st = st.accumulate(self_id(st), other_id, message, xml_cache) - val execs1 = execs + (id -> new_st) - (new_st, copy(execs = execs1, commands_redirection = redirection(new_st))) + def update(st: Command.State): (Command.State, State) = + { + val st1 = st.accumulate(self_id(st), other_id, message, xml_cache) + (st1, copy(commands_redirection = redirection(st1))) + } + execs.get(id).map(update) match { + case Some((st1, state1)) => (st1, state1.copy(execs = execs + (id -> st1))) case None => - commands.get(id) match { - case Some(st) => - val new_st = st.accumulate(self_id(st), other_id, message, xml_cache) - val commands1 = commands + (id -> new_st) - (new_st, copy(commands = commands1, commands_redirection = redirection(new_st))) - case None => fail + commands.get(id).map(update) match { + case Some((st1, state1)) => (st1, state1.copy(commands = commands + (id -> st1))) + case None => + theories.get(id).map(update) match { + case Some((st1, state1)) => (st1, state1.copy(theories = theories + (id -> st1))) + case None => fail + } } } } @@ -781,6 +809,27 @@ st <- command_states(version, command).iterator } yield st.exports) + def begin_theory(node_name: Node.Name, id: Document_ID.Exec, source: String): State = + if (theories.isDefinedAt(id)) fail + else { + val command = Command.unparsed(source, theory = true, id = id, node_name = node_name) + copy(theories = theories + (id -> command.empty_state)) + } + + def end_theory(theory: String): (Snapshot, State) = + theories.collectFirst({ case (_, st) if st.command.node_name.theory == theory => st }) match { + case None => fail + case Some(st) => + val command = st.command + val node_name = command.node_name + val command1 = + Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name, + results = st.results, markups = st.markups) + val state1 = copy(theories = theories - command1.id) + val snapshot = state1.snapshot(name = node_name).command_snippet(command1) + (snapshot, state1) + } + def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) : ((List[Node.Name], List[Command]), State) = { @@ -955,11 +1004,11 @@ range: Text.Range, elements: Markup.Elements): Markup_Tree = Command.State.merge_markup(command_states(version, command), index, range, elements) - def markup_to_XML( + def xml_markup( version: Version, node_name: Node.Name, - range: Text.Range, - elements: Markup.Elements): XML.Body = + range: Text.Range = Text.Range.full, + elements: Markup.Elements = Markup.Elements.full): XML.Body = { val node = version.nodes(node_name) if (node_name.is_theory) { @@ -1079,8 +1128,10 @@ } else version.nodes.commands_loading(other_node_name).headOption - def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body = - state.markup_to_XML(version, node_name, range, elements) + def xml_markup( + range: Text.Range = Text.Range.full, + elements: Markup.Elements = Markup.Elements.full): XML.Body = + state.xml_markup(version, node_name, range = range, elements = elements) lazy val messages: List[(XML.Tree, Position.T)] = (for { diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/PIDE/markup.ML Thu Nov 26 18:09:15 2020 +0000 @@ -59,8 +59,8 @@ val end_offsetN: string val fileN: string val idN: string - val position_properties': string list val position_properties: string list + val position_property: Properties.entry -> bool val positionN: string val position: T val expressionN: string val expression: string -> T val citationN: string val citation: string -> T @@ -220,6 +220,7 @@ val theory_timing: Properties.entry val session_timing: Properties.entry val loading_theory: string -> Properties.T + val finished_theory: string -> Properties.T val build_session_finished: Properties.T val print_operationsN: string val print_operations: Properties.T @@ -379,8 +380,8 @@ val fileN = "file"; val idN = "id"; -val position_properties' = [fileN, idN]; -val position_properties = [lineN, offsetN, end_offsetN] @ position_properties'; +val position_properties = [lineN, offsetN, end_offsetN, fileN, idN]; +fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry); val (positionN, position) = markup_elem "position"; @@ -692,7 +693,8 @@ val session_timing = (functionN, "session_timing"); -fun loading_theory name = [("function", "loading_theory"), ("name", name)]; +fun loading_theory name = [("function", "loading_theory"), (nameN, name)]; +fun finished_theory name = [("function", "finished_theory"), (nameN, name)]; val build_session_finished = [("function", "build_session_finished")]; diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/PIDE/markup.scala Thu Nov 26 18:09:15 2020 +0000 @@ -144,6 +144,8 @@ val DEF_ID = "def_id" val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) + def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1) + val POSITION = "position" @@ -587,6 +589,7 @@ } val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name) + def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1) object Command_Timing extends Properties_Function("command_timing") object Theory_Timing extends Properties_Function("theory_timing") @@ -596,7 +599,8 @@ } object Task_Statistics extends Properties_Function("task_statistics") - object Loading_Theory extends Name_Function("loading_theory") + object Loading_Theory extends Properties_Function("loading_theory") + object Finished_Theory extends Name_Function("finished_theory") object Build_Session_Finished extends Function("build_session_finished") object Commands_Accepted extends Function("commands_accepted") diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/PIDE/protocol.scala Thu Nov 26 18:09:15 2020 +0000 @@ -21,6 +21,21 @@ val Error_Message_Marker = Protocol_Message.Marker("error_message") + /* batch build */ + + object Loading_Theory + { + def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] = + (props, props, props) match { + case (Markup.Name(name), Position.File(file), Position.Id(id)) + if Path.is_wellformed(file) => + val master_dir = Path.explode(file).dir.implode + Some((Document.Node.Name(file, master_dir, name), id)) + case _ => None + } + } + + /* document editing */ object Commands_Accepted @@ -188,13 +203,13 @@ object Export { sealed case class Args( - id: Option[String], - serial: Long, + id: Option[String] = None, + serial: Long = 0L, theory_name: String, name: String, - executable: Boolean, - compress: Boolean, - strict: Boolean) + executable: Boolean = false, + compress: Boolean = true, + strict: Boolean = true) { def compound_name: String = isabelle.Export.compound_name(theory_name, name) } diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/PIDE/protocol_message.scala --- a/src/Pure/PIDE/protocol_message.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/PIDE/protocol_message.scala Thu Nov 26 18:09:15 2020 +0000 @@ -71,50 +71,4 @@ case XML.Elem(_, ts) => reports(props, ts) case XML.Text(_) => Nil } - - - /* reported positions */ - - private val position_elements = - Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) - - def positions( - self_id: Document_ID.Generic => Boolean, - command_position: Position.T, - chunk_name: Symbol.Text_Chunk.Name, - chunk: Symbol.Text_Chunk, - message: XML.Elem): Set[Text.Range] = - { - def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = - props match { - case Position.Identified(id, name) if self_id(id) && name == chunk_name => - val opt_range = - Position.Range.unapply(props) orElse { - if (name == Symbol.Text_Chunk.Default) - Position.Range.unapply(command_position) - else None - } - opt_range match { - case Some(symbol_range) => - chunk.incorporate(symbol_range) match { - case Some(range) => set + range - case _ => set - } - case None => set - } - case _ => set - } - def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] = - t match { - case XML.Wrapped_Elem(Markup(name, props), _, body) => - body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree) - case XML.Elem(Markup(name, props), body) => - body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree) - case XML.Text(_) => set - } - - val set = tree(Set.empty, message) - if (set.isEmpty) elem(message.markup.properties, set) - else set - } } diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/PIDE/rendering.scala Thu Nov 26 18:09:15 2020 +0000 @@ -97,8 +97,8 @@ def output_messages(results: Command.Results): List[XML.Tree] = { val (states, other) = - results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList - .partition(Protocol.is_state(_)) + results.iterator.map(_._2).filterNot(Protocol.is_result).toList + .partition(Protocol.is_state) states ::: other } @@ -169,6 +169,9 @@ /* markup elements */ + val position_elements = + Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) + val semantic_completion_elements = Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) @@ -293,13 +296,13 @@ Some(Completion.Language_Context.inner) }).headOption.map(_.info) - def citation(range: Text.Range): Option[Text.Info[String]] = + def citations(range: Text.Range): List[Text.Info[String]] = snapshot.select(range, Rendering.citation_elements, _ => { case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => Some(Text.Info(snapshot.convert(info_range), name)) case _ => None - }).headOption.map(_.info) + }).map(_.info) /* file-system path completion */ diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/PIDE/session.scala Thu Nov 26 18:09:15 2020 +0000 @@ -181,6 +181,7 @@ /* outlets */ + val finished_theories = new Session.Outlet[Document.Snapshot](dispatcher) val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher) val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher) val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher) @@ -475,7 +476,9 @@ { try { val st = global_state.change_result(f) - change_buffer.invoke(false, Nil, List(st.command)) + if (!st.command.span.is_theory) { + change_buffer.invoke(false, Nil, List(st.command)) + } } catch { case _: Document.State.Fail => bad_output() } } @@ -502,6 +505,17 @@ val export = Export.make_entry("", args, msg.bytes, cache = xz_cache) change_command(_.add_export(id, (args.serial, export))) + case Protocol.Loading_Theory(node_name, id) => + try { global_state.change(_.begin_theory(node_name, id, msg.text)) } + catch { case _: Document.State.Fail => bad_output() } + + case Markup.Finished_Theory(theory) => + try { + val snapshot = global_state.change_result(_.end_theory(theory)) + finished_theories.post(snapshot) + } + catch { case _: Document.State.Fail => bad_output() } + case List(Markup.Commands_Accepted.PROPERTY) => msg.text match { case Protocol.Commands_Accepted(ids) => diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/ROOT.ML Thu Nov 26 18:09:15 2020 +0000 @@ -352,3 +352,4 @@ ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML" + diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/System/isabelle_process.ML Thu Nov 26 18:09:15 2020 +0000 @@ -148,11 +148,10 @@ if forall (fn s => s = "") ss then () else let - val props' = - (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of - (false, SOME id') => props @ [(Markup.idN, id')] - | _ => props); - in message name props' (XML.blob ss) end; + val pos_props = + if exists Markup.position_property props then props + else props @ Position.properties_of (Position.thread_data ()); + in message name pos_props (XML.blob ss) end; fun report_message ss = if Context_Position.pide_reports () diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/System/process_result.scala Thu Nov 26 18:09:15 2020 +0000 @@ -53,6 +53,9 @@ def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1) + def errors_rc(errs: List[String]): Process_Result = + if (errs.isEmpty) this else errors(errs).error_rc + def check_rc(pred: Int => Boolean): Process_Result = if (pred(rc)) this else if (interrupted) throw Exn.Interrupt() diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/System/progress.scala Thu Nov 26 18:09:15 2020 +0000 @@ -32,7 +32,6 @@ def echo_warning(msg: String) { echo(Output.warning_text(msg)) } def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) } - def echo_document(msg: String) { echo(msg) } def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A = Timing.timeit(message, enabled, echo)(e) diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Thy/bibtex.scala Thu Nov 26 18:09:15 2020 +0000 @@ -191,7 +191,7 @@ models: Map[A, B]): Option[Completion.Result] = { for { - Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret)) + Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption name1 <- Completion.clean_name(name) original <- rendering.model.get_text(r) diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Thy/export.scala Thu Nov 26 18:09:15 2020 +0000 @@ -13,7 +13,14 @@ object Export { - /* name structure */ + /* artefact names */ + + val MARKUP = "PIDE/markup" + val MESSAGES = "PIDE/messages" + val DOCUMENT_PREFIX = "document/" + val CITATIONS = DOCUMENT_PREFIX + "citations" + val THEORY_PREFIX: String = "theory/" + val PROOFS_PREFIX: String = "proofs/" def explode_name(s: String): List[String] = space_explode('/', s) def implode_name(elems: Iterable[String]): String = elems.mkString("/") @@ -89,6 +96,7 @@ def compound_name: String = Export.compound_name(theory_name, name) + def name_has_prefix(s: String): Boolean = name.startsWith(s) val name_elems: List[String] = explode_name(name) def name_extends(elems: List[String]): Boolean = diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Thy/export_theory.scala Thu Nov 26 18:09:15 2020 +0000 @@ -62,9 +62,6 @@ /** theory content **/ - val export_prefix: String = "theory/" - val export_prefix_proofs: String = "proofs/" - sealed case class Theory(name: String, parents: List[String], types: List[Type], consts: List[Const], @@ -115,7 +112,7 @@ val parents = if (theory_name == Thy_Header.PURE) Nil else { - provider(export_prefix + "parents") match { + provider(Export.THEORY_PREFIX + "parents") match { case Some(entry) => split_lines(entry.uncompressed().text) case None => error("Missing theory export in session " + quote(session_name) + ": " + @@ -195,7 +192,7 @@ case XML.Elem(Markup(Markup.ENTITY, props), body) => val name = Markup.Name.unapply(props) getOrElse err() val xname = Markup.XName.unapply(props) getOrElse err() - val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID }) + val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID) val id = Position.Id.unapply(props) val serial = Markup.Serial.unapply(props) getOrElse err() (Entity(kind, name, xname, pos, id, serial), body) @@ -239,7 +236,7 @@ } def read_types(provider: Export.Provider): List[Type] = - provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) => + provider.uncompressed_yxml(Export.THEORY_PREFIX + "types").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.TYPE, tree) val (syntax, args, abbrev) = @@ -271,7 +268,7 @@ } def read_consts(provider: Export.Provider): List[Const] = - provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) => + provider.uncompressed_yxml(Export.THEORY_PREFIX + "consts").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.CONST, tree) val (syntax, (typargs, (typ, (abbrev, propositional)))) = @@ -318,7 +315,7 @@ } def read_axioms(provider: Export.Provider): List[Axiom] = - provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) => + provider.uncompressed_yxml(Export.THEORY_PREFIX + "axioms").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.AXIOM, tree) val prop = decode_prop(body) @@ -348,7 +345,7 @@ } def read_thms(provider: Export.Provider): List[Thm] = - provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) => + provider.uncompressed_yxml(Export.THEORY_PREFIX + "thms").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.THM, tree) val (prop, deps, prf) = @@ -379,7 +376,7 @@ def read_proof( provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] = { - for { entry <- provider.focus(id.theory_name)(export_prefix_proofs + id.serial) } + for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) } yield { val body = entry.uncompressed_yxml() val (typargs, (args, (prop_body, proof_body))) = @@ -454,7 +451,7 @@ } def read_classes(provider: Export.Provider): List[Class] = - provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) => + provider.uncompressed_yxml(Export.THEORY_PREFIX + "classes").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.CLASS, tree) val (params, axioms) = @@ -483,7 +480,7 @@ } def read_locales(provider: Export.Provider): List[Locale] = - provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) => + provider.uncompressed_yxml(Export.THEORY_PREFIX + "locales").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.LOCALE, tree) val (typargs, args, axioms) = @@ -520,7 +517,7 @@ } def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] = - provider.uncompressed_yxml(export_prefix + "locale_dependencies").map((tree: XML.Tree) => + provider.uncompressed_yxml(Export.THEORY_PREFIX + "locale_dependencies").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.LOCALE_DEPENDENCY, tree) val (source, (target, (prefix, (subst_types, subst_terms)))) = @@ -544,7 +541,7 @@ def read_classrel(provider: Export.Provider): List[Classrel] = { - val body = provider.uncompressed_yxml(export_prefix + "classrel") + val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "classrel") val classrel = { import XML.Decode._ @@ -562,7 +559,7 @@ def read_arities(provider: Export.Provider): List[Arity] = { - val body = provider.uncompressed_yxml(export_prefix + "arities") + val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "arities") val arities = { import XML.Decode._ @@ -583,7 +580,7 @@ def read_constdefs(provider: Export.Provider): List[Constdef] = { - val body = provider.uncompressed_yxml(export_prefix + "constdefs") + val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs") val constdefs = { import XML.Decode._ @@ -609,7 +606,7 @@ def read_typedefs(provider: Export.Provider): List[Typedef] = { - val body = provider.uncompressed_yxml(export_prefix + "typedefs") + val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs") val typedefs = { import XML.Decode._ @@ -645,7 +642,7 @@ def read_datatypes(provider: Export.Provider): List[Datatype] = { - val body = provider.uncompressed_yxml(export_prefix + "datatypes") + val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes") val datatypes = { import XML.Decode._ @@ -741,7 +738,7 @@ def read_spec_rules(provider: Export.Provider): List[Spec_Rule] = { - val body = provider.uncompressed_yxml(export_prefix + "spec_rules") + val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules") val spec_rules = { import XML.Decode._ diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Thy/presentation.scala Thu Nov 26 18:09:15 2020 +0000 @@ -12,9 +12,15 @@ object Presentation { - /* document variants */ + /* document info */ - type Document_PDF = (Document_Variant, Bytes) + abstract class Document_Name + { + def name: String + def path: Path = Path.basic(name) + + override def toString: String = name + } object Document_Variant { @@ -29,13 +35,11 @@ } } - sealed case class Document_Variant(name: String, tags: List[String], sources: String = "") + sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name { def print_tags: String = tags.mkString(",") def print: String = if (tags.isEmpty) name else name + "=" + print_tags - def path: Path = Path.basic(name) - def latex_sty: String = Library.terminate_lines( tags.map(tag => @@ -45,8 +49,19 @@ case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" case cs => "\\isakeeptag{" + cs.mkString + "}" })) + } - def set_sources(s: String): Document_Variant = copy(sources = s) + sealed case class Document_Input(name: String, sources: SHA1.Digest) + extends Document_Name + + sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes) + extends Document_Name + { + def log: String = log_xz.uncompress().text + def log_lines: List[String] = split_lines(log) + + def write(db: SQL.Database, session_name: String) = + write_document(db, session_name, this) } @@ -56,32 +71,30 @@ { val session_name = SQL.Column.string("session_name").make_primary_key val name = SQL.Column.string("name").make_primary_key - val tags = SQL.Column.string("tags") val sources = SQL.Column.string("sources") + val log_xz = SQL.Column.bytes("log_xz") val pdf = SQL.Column.bytes("pdf") - val table = SQL.Table("isabelle_documents", List(session_name, name, tags, sources, pdf)) + val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf)) def where_equal(session_name: String, name: String = ""): SQL.Source = "WHERE " + Data.session_name.equal(session_name) + (if (name == "") "" else " AND " + Data.name.equal(name)) } - def read_document_variants(db: SQL.Database, session_name: String): List[Document_Variant] = + def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = { - val select = - Data.table.select(List(Data.name, Data.tags, Data.sources), Data.where_equal(session_name)) + val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name)) db.using_statement(select)(stmt => stmt.execute_query().iterator(res => { val name = res.string(Data.name) - val tags = res.string(Data.tags) val sources = res.string(Data.sources) - Document_Variant.parse(name, tags).set_sources(sources) + Document_Input(name, SHA1.fake(sources)) }).toList) } - def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_PDF] = + def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] = { val select = Data.table.select(sql = Data.where_equal(session_name, name)) db.using_statement(select)(stmt => @@ -89,24 +102,24 @@ val res = stmt.execute_query() if (res.next()) { val name = res.string(Data.name) - val tags = res.string(Data.tags) val sources = res.string(Data.sources) + val log_xz = res.bytes(Data.log_xz) val pdf = res.bytes(Data.pdf) - Some(Document_Variant.parse(name, tags).set_sources(sources) -> pdf) + Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf)) } else None }) } - def write_document(db: SQL.Database, session_name: String, doc: Document_Variant, pdf: Bytes) + def write_document(db: SQL.Database, session_name: String, doc: Document_Output) { db.using_statement(Data.table.insert())(stmt => { stmt.string(1) = session_name stmt.string(2) = doc.name - stmt.string(3) = doc.print_tags - stmt.string(4) = doc.sources - stmt.bytes(5) = pdf + stmt.string(3) = doc.sources.toString + stmt.bytes(4) = doc.log_xz + stmt.bytes(5) = doc.pdf stmt.execute() }) } @@ -253,8 +266,8 @@ val documents = for { doc <- info.document_variants - (_, pdf) <- db_context.read_document(session, doc.name) - } yield { Bytes.write(session_dir + doc.path.pdf, pdf); doc } + document <- db_context.input_database(session)(read_document(_, _, doc.name)) + } yield { Bytes.write(session_dir + doc.path.pdf, document.pdf); doc } val links = { @@ -424,7 +437,7 @@ } def pide_document(snapshot: Document.Snapshot): XML.Body = - make_html(snapshot.markup_to_XML(Text.Range.full, document_elements)) + make_html(snapshot.xml_markup(elements = document_elements)) @@ -443,7 +456,7 @@ output_sources: Option[Path] = None, output_pdf: Option[Path] = None, verbose: Boolean = false, - verbose_latex: Boolean = false): List[Document_PDF] = + verbose_latex: Boolean = false): List[Document_Output] = { /* session info */ @@ -499,7 +512,7 @@ yield { Isabelle_System.with_tmp_dir("document")(tmp_dir => { - progress.echo_document("Building document " + session + "/" + doc.name + " ...") + progress.echo("Preparing " + session + "/" + doc.name + " ...") val start = Time.now() @@ -507,7 +520,7 @@ val (doc_dir, root) = prepare_dir1(tmp_dir, doc) val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest) - val sources = SHA1.digest_set(digests).toString + val sources = SHA1.digest_set(digests) prepare_dir2(tmp_dir, doc) for (dir <- output_sources) { @@ -520,12 +533,12 @@ val old_document = for { - document@(doc, pdf) <- db_context.read_document(session, doc.name) - if doc.sources == sources + old_doc <- db_context.input_database(session)(read_document(_, _, doc.name)) + if old_doc.sources == sources } yield { - Bytes.write(doc_dir + doc.path.pdf, pdf) - document + Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf) + old_doc } old_document getOrElse { @@ -574,20 +587,22 @@ else { val stop = Time.now() val timing = stop - start - progress.echo_document("Finished document " + session + "/" + doc.name + + progress.echo("Finished " + session + "/" + doc.name + " (" + timing.message_hms + " elapsed time)") - doc.set_sources(sources) -> Bytes.read(result_path) + val log_xz = Bytes(cat_lines(result.out_lines ::: result.err_lines)).compress() + val pdf = Bytes.read(result_path) + Document_Output(doc.name, sources, log_xz, pdf) } } }) } - for (dir <- output_pdf; (doc, pdf) <- documents) { + for (dir <- output_pdf; doc <- documents) { Isabelle_System.make_directory(dir) val path = dir + doc.path.pdf - Bytes.write(path, pdf) - progress.echo_document("Document at " + path.absolute) + Bytes.write(path, doc.pdf) + progress.echo("Document at " + path.absolute) } documents diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Thy/sessions.scala Thu Nov 26 18:09:15 2020 +0000 @@ -1190,6 +1190,22 @@ def close { database_server.foreach(_.close) } + def output_database[A](session: String)(f: SQL.Database => A): A = + database_server match { + case Some(db) => f(db) + case None => using(store.open_database(session, output = true))(f) + } + + def input_database[A](session: String)(f: (SQL.Database, String) => Option[A]): Option[A] = + database_server match { + case Some(db) => f(db, session) + case None => + store.try_open_database(session) match { + case Some(db) => using(db)(f(_, session)) + case None => None + } + } + def read_export(session: String, theory_name: String, name: String): Option[Export.Entry] = { val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view @@ -1211,16 +1227,6 @@ read_export(session, theory_name, name) getOrElse Export.empty_entry(session, theory_name, name) - def read_document(session_name: String, name: String): Option[Presentation.Document_PDF] = - database_server match { - case Some(db) => Presentation.read_document(db, session_name, name) - case None => - store.try_open_database(session_name) match { - case Some(db) => using(db)(Presentation.read_document(_, session_name, name)) - case None => None - } - } - override def toString: String = { val s = diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Thy/thy_info.ML Thu Nov 26 18:09:15 2020 +0000 @@ -56,7 +56,8 @@ ); fun apply_presentation (context: presentation_context) thy = - ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); + (ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); + Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) []); fun add_presentation f = Presentation.map (cons (f, stamp ())); @@ -292,7 +293,7 @@ val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; -fun eval_thy options update_time master_dir header text_pos text parents = +fun eval_thy options master_dir header text_pos text parents = let val (name, _) = #name header; val keywords = @@ -324,30 +325,32 @@ fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; -fun load_thy options initiators update_time deps text (name, pos) keywords parents = +fun load_thy options initiators deps text (name, pos) keywords parents = let - val _ = remove_thy name; - val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); - val _ = Output.try_protocol_message (Markup.loading_theory name) []; + val exec_id = Document_ID.make (); + val id = Document_ID.print exec_id; + val _ = + Execution.running Document_ID.none exec_id [] orelse + raise Fail ("Failed to register execution: " ^ id); val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val header = Thy_Header.make (name, pos) imports keywords; - val _ = (imports ~~ parents) |> List.app (fn ((_, pos), thy) => Context_Position.reports_global thy [(pos, Theory.get_markup thy)]); - val exec_id = Document_ID.make (); - val _ = - Execution.running Document_ID.none exec_id [] orelse - raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); + val text_pos = Position.put_id id (Path.position thy_path); + val text_props = Position.properties_of text_pos; + + val _ = remove_thy name; + val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); + val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) (XML.blob [text]); val timing_start = Timing.start (); - val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); val (theory, present, weight) = - eval_thy options update_time dir header text_pos text + eval_thy options dir header text_pos text (if name = Context.PureN then [Context.the_global_context ()] else parents); val timing_result = Timing.result timing_start; @@ -411,12 +414,8 @@ (case deps of NONE => raise Fail "Malformed deps" | SOME (dep, text) => - let - val update_time = serial (); - val load = - load_thy options initiators update_time - dep text (theory_name, theory_pos) keywords; - in Task (parents, load) end); + Task (parents, + load_thy options initiators dep text (theory_name, theory_pos) keywords)); val tasks'' = new_entry theory_name parents task tasks'; in (all_current, tasks'') end) diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Tools/build.scala Thu Nov 26 18:09:15 2020 +0000 @@ -202,7 +202,7 @@ options + "completion_limit=0" + "editor_tracing_messages=0" + - "pide_reports=false" + ("pide_reports=" + options.bool("build_pide_reports")) val store = Sessions.store(build_options) @@ -429,7 +429,7 @@ val numa_node = numa_nodes.next(used_node) val job = - new Build_Job(progress, session_name, info, deps, store, do_store, presentation, + new Build_Job(progress, session_name, info, deps, store, do_store, verbose, numa_node, queue.command_timings(session_name)) loop(pending, running + (session_name -> (ancestor_heaps, job)), results) } diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Tools/build_job.scala Thu Nov 26 18:09:15 2020 +0000 @@ -16,7 +16,6 @@ deps: Sessions.Deps, store: Sessions.Store, do_store: Boolean, - presentation: Presentation.Context, verbose: Boolean, val numa_node: Option[Int], command_timings0: List[Properties.T]) @@ -52,6 +51,10 @@ override val xml_cache: XML.Cache = store.xml_cache override val xz_cache: XZ.Cache = store.xz_cache } + def make_rendering(snapshot: Document.Snapshot): Rendering = + new Rendering(snapshot, options, session) { + override def model: Document.Model = ??? + } object Build_Session_Errors { @@ -77,7 +80,6 @@ val session_timings = new mutable.ListBuffer[Properties.T] val runtime_statistics = new mutable.ListBuffer[Properties.T] val task_statistics = new mutable.ListBuffer[Properties.T] - val document_output = new mutable.ListBuffer[String] def fun( name: String, @@ -120,9 +122,9 @@ private def loading_theory(msg: Prover.Protocol_Output): Boolean = msg.properties match { - case Markup.Loading_Theory(name) => + case Markup.Loading_Theory(Markup.Name(name)) => progress.theory(Progress.Theory(name, session = session_name)) - true + false case _ => false } @@ -134,30 +136,53 @@ case _ => false } - private def command_timing(props: Properties.T): Option[Properties.T] = - for { - props1 <- Markup.Command_Timing.unapply(props) - elapsed <- Markup.Elapsed.unapply(props1) - elapsed_time = Time.seconds(elapsed) - if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") - } yield props1.filter(p => Markup.command_timing_properties(p._1)) - override val functions = List( Markup.Build_Session_Finished.name -> build_session_finished, Markup.Loading_Theory.name -> loading_theory, Markup.EXPORT -> export, - fun(Markup.Command_Timing.name, command_timings, command_timing), fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) }) + session.command_timings += Session.Consumer("command_timings") + { + case Session.Command_Timing(props) => + for { + elapsed <- Markup.Elapsed.unapply(props) + elapsed_time = Time.seconds(elapsed) + if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") + } command_timings += props.filter(Markup.command_timing_property) + } + session.runtime_statistics += Session.Consumer("ML_statistics") { case Session.Runtime_Statistics(props) => runtime_statistics += props } + session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") + { + case snapshot => + val rendering = make_rendering(snapshot) + + def export(name: String, xml: XML.Body) + { + val theory_name = snapshot.node_name.theory + val args = Protocol.Export.Args(theory_name = theory_name, name = name) + val bytes = Bytes(YXML.string_of_body(xml)) + if (!bytes.is_empty) export_consumer(session_name, args, bytes) + } + def export_text(name: String, text: String): Unit = + export(name, List(XML.Text(text))) + + export(Export.MARKUP, snapshot.xml_markup()) + export(Export.MESSAGES, snapshot.messages.map(_._1)) + + val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info)) + export_text(Export.CITATIONS, cat_lines(citations)) + } + session.all_messages += Session.Consumer[Any]("build_session_output") { case msg: Prover.Output => @@ -212,38 +237,31 @@ val process_result = Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown } + session.stop() + val export_errors = export_consumer.shutdown(close = true).map(Output.error_message_text) - val document_errors = + val (document_output, document_errors) = try { if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { - val document_progress = - new Progress { - override def echo(msg: String): Unit = - document_output.synchronized { document_output += msg } - override def echo_document(msg: String): Unit = - progress.echo_document(msg) - } - val documents = - using(store.open_database_context(deps.sessions_structure))(db_context => - Presentation.build_documents(session_name, deps, db_context, - output_sources = info.document_output, - output_pdf = info.document_output, - progress = document_progress, - verbose = verbose, - verbose_latex = true)) - using(store.open_database(session_name, output = true))(db => - for ((doc, pdf) <- documents) { - db.transaction { - Presentation.write_document(db, session_name, doc, pdf) - } + using(store.open_database_context(deps.sessions_structure))(db_context => + { + val documents = + Presentation.build_documents(session_name, deps, db_context, + output_sources = info.document_output, + output_pdf = info.document_output, + progress = progress, + verbose = verbose) + db_context.output_database(session_name)(db => + documents.foreach(_.write(db, session_name))) + (documents.flatMap(_.log_lines), Nil) }) } - Nil + (Nil, Nil) } - catch { case Exn.Interrupt.ERROR(msg) => List(msg) } + catch { case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) } val result = { @@ -256,12 +274,11 @@ session_timings.toList.map(Protocol.Session_Timing_Marker.apply) ::: runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: - document_output.toList + document_output - val more_errors = - Library.trim_line(stderr.toString) :: export_errors ::: document_errors - - process_result.output(more_output).errors(more_errors) + process_result.output(more_output) + .error(Library.trim_line(stderr.toString)) + .errors_rc(export_errors ::: document_errors) } build_errors match { diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Tools/dump.scala Thu Nov 26 18:09:15 2020 +0000 @@ -48,27 +48,22 @@ val known_aspects: List[Aspect] = List( Aspect("markup", "PIDE markup (YXML format)", - { case args => - args.write(Path.explode("markup.yxml"), - args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full)) - }), + args => args.write(Path.explode(Export.MARKUP), args.snapshot.xml_markup())), Aspect("messages", "output messages (YXML format)", - { case args => - args.write(Path.explode("messages.yxml"), - args.snapshot.messages.iterator.map(_._1).toList) - }), + args => args.write(Path.explode(Export.MESSAGES), args.snapshot.messages.map(_._1))), Aspect("latex", "generated LaTeX source", - { case args => - for (entry <- args.snapshot.exports if entry.name == "document.tex") - args.write(Path.explode(entry.name), entry.uncompressed()) - }), + args => + for { + entry <- args.snapshot.exports + if entry.name_has_prefix(Export.DOCUMENT_PREFIX) + } args.write(Path.explode(entry.name), entry.uncompressed())), Aspect("theory", "foundational theory content", - { case args => - for { - entry <- args.snapshot.exports - if entry.name.startsWith(Export_Theory.export_prefix) - } args.write(Path.explode(entry.name), entry.uncompressed()) - }, options = List("export_theory")) + args => + for { + entry <- args.snapshot.exports + if entry.name_has_prefix(Export.THEORY_PREFIX) + } args.write(Path.explode(entry.name), entry.uncompressed()), + options = List("export_theory")) ).sortBy(_.name) def show_aspects: String = diff -r bbe5d3ef2052 -r 7553c1880815 src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Pure/Tools/update.scala Thu Nov 26 18:09:15 2020 +0000 @@ -45,8 +45,8 @@ val snapshot = args.snapshot for ((node_name, node) <- snapshot.nodes) { val xml = - snapshot.state.markup_to_XML(snapshot.version, node_name, - Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)) + snapshot.state.xml_markup(snapshot.version, node_name, + elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)) val source1 = Symbol.encode(XML.content(update_xml(xml))) if (source1 != Symbol.encode(node.source)) { diff -r bbe5d3ef2052 -r 7553c1880815 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Thu Nov 26 18:09:15 2020 +0000 @@ -21,9 +21,21 @@ object JEdit_Rendering { + /* make rendering */ + def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering = new JEdit_Rendering(snapshot, model, options) + def text(snapshot: Document.Snapshot, formatted_body: XML.Body, + results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) = + { + val command = Command.rich_text(Document_ID.make(), results, formatted_body) + val snippet = snapshot.command_snippet(command) + val model = File_Model.empty(PIDE.session) + val rendering = apply(snippet, model, PIDE.options.value) + (command.source, rendering) + } + /* popup window bounds */ diff -r bbe5d3ef2052 -r 7553c1880815 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 26 18:09:02 2020 +0000 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 26 18:09:15 2020 +0000 @@ -27,42 +27,6 @@ import org.gjt.sp.util.{SyntaxUtilities, Log} -object Pretty_Text_Area -{ - /* auxiliary */ - - private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results, - formatted_body: XML.Body): (String, Document.State) = - { - val command = Command.rich_text(Document_ID.make(), base_results, formatted_body) - val node_name = command.node_name - val edits: List[Document.Edit_Text] = - List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source)))) - - val state0 = base_snapshot.state.define_command(command) - val version0 = base_snapshot.version - val nodes0 = version0.nodes - - val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) - val version1 = Document.Version.make(nodes1) - val state1 = - state0.continue_history(Future.value(version0), edits, Future.value(version1)) - .define_version(version1, state0.the_assignment(version0)) - .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2 - - (command.source, state1) - } - - private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results, - formatted_body: XML.Body): (String, JEdit_Rendering) = - { - val (text, state) = document_state(base_snapshot, base_results, formatted_body) - val model = File_Model.empty(PIDE.session) - val rendering = JEdit_Rendering(state.snapshot(), model, PIDE.options.value) - (text, rendering) - } -} - class Pretty_Text_Area( view: View, close_action: () => Unit = () => (), @@ -77,7 +41,7 @@ private var current_base_snapshot = Document.Snapshot.init private var current_base_results = Command.Results.empty private var current_rendering: JEdit_Rendering = - Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2 + JEdit_Rendering.text(current_base_snapshot, Nil)._2 private var future_refresh: Option[Future[Unit]] = None private val rich_text_area = @@ -112,7 +76,7 @@ getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor")) getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor")) - get_background().map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) }) + get_background().foreach(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) }) getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor")) getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor")) getGutter.setFont(jEdit.getFontProperty("view.gutter.font")) @@ -127,15 +91,15 @@ val metric = JEdit_Lib.pretty_metric(getPainter) val margin = (getPainter.getWidth.toDouble / metric.unit) max 20.0 - val base_snapshot = current_base_snapshot - val base_results = current_base_results + val snapshot = current_base_snapshot + val results = current_base_results val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric) - future_refresh.map(_.cancel) + future_refresh.foreach(_.cancel) future_refresh = Some(Future.fork { val (text, rendering) = - try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) } + try { JEdit_Rendering.text(snapshot, formatted_body, results = results) } catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn } Exn.Interrupt.expose()