--- 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 /
--- 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"
--- 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]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
by (auto simp: invar_def invar_bheap_merge invar_oheap_merge)
--- /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 \<open>Heaps\<close>
+
+theory Heaps
+imports
+ "HOL-Library.Tree_Multiset"
+ Priority_Queue_Specs
+begin
+
+text \<open>Heap = priority queue on trees:\<close>
+
+locale Heap =
+fixes insert :: "('a::linorder) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
+and del_min :: "'a tree \<Rightarrow> 'a tree"
+assumes mset_insert: "heap q \<Longrightarrow> mset_tree (insert x q) = {#x#} + mset_tree q"
+and mset_del_min: "\<lbrakk> heap q; q \<noteq> Leaf \<rbrakk> \<Longrightarrow> mset_tree (del_min q) = mset_tree q - {#value q#}"
+and heap_insert: "heap q \<Longrightarrow> heap(insert x q)"
+and heap_del_min: "heap q \<Longrightarrow> heap(del_min q)"
+begin
+
+definition empty :: "'a tree" where
+"empty = Leaf"
+
+fun is_empty :: "'a tree \<Rightarrow> 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 \<open>Once you have \<open>merge\<close>, \<open>insert\<close> and \<open>del_min\<close> are easy:\<close>
+
+locale Heap_Merge =
+fixes merge :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
+assumes mset_merge: "\<lbrakk> heap q1; heap q2 \<rbrakk> \<Longrightarrow> mset_tree (merge q1 q2) = mset_tree q1 + mset_tree q2"
+and invar_merge: "\<lbrakk> heap q1; heap q2 \<rbrakk> \<Longrightarrow> heap (merge q1 q2)"
+begin
+
+fun insert :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"insert x t = merge (Node Leaf x Leaf) t"
+
+fun del_min :: "'a tree \<Rightarrow> '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
--- 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"
--- 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)
--- 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
--- 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] =
--- 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;
--- 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 =
--- 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)
}
--- 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 "<command>"
case Ignored_Span => "<ignored>"
case Malformed_Span => "<malformed>"
+ case Theory_Span => "<theory>"
}
}
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 */
--- 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 {
--- 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")];
--- 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")
--- 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)
}
--- 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
- }
}
--- 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 */
--- 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) =>
--- 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"
+
--- 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 ()
--- 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()
--- 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)
--- 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)
--- 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 =
--- 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._
--- 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
--- 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 =
--- 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)
--- 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)
}
--- 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 {
--- 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 =
--- 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)) {
--- 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 */
--- 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()