--- a/NEWS Wed Aug 06 16:51:58 2025 +0200
+++ b/NEWS Wed Aug 06 17:39:03 2025 +0200
@@ -31,7 +31,9 @@
database. Example: "isabelle jedit -l HOL src/HOL/Nat.thy" for theory
"HOL.Nat" in session "HOL". This information is read-only: editing
theory sources in the editor will invalidate formal markup, and replace
-it by an error message.
+it by an error message. Output messages exclude proof states and final
+results, unless the underlying session database has been built with
+option "show_states".
*** Isabelle/jEdit Prover IDE ***
@@ -92,11 +94,8 @@
*** Pure ***
-* Command 'thy_deps' expects optional theory arguments as long theory names,
-the same way as the 'imports' clause. Minor INCOMPATIBILITY.
-
-* ML function 'Raw_Simplifier.rewrite' renamed to 'Raw_Simplifier.rewrite_wrt',
-to avoid clash with existing 'Simplifier.rewrite'. INCOMPATIBILITY.
+* Command 'thy_deps' expects optional theory arguments as long theory
+names, the same way as the 'imports' clause. Minor INCOMPATIBILITY.
*** HOL ***
@@ -139,22 +138,25 @@
const [List.]map_project ~> Option.image_filter
thm map_project_def ~> Option.image_filter_eq
-The _def suffix for characteristic theorems is avoided to emphasize that these
-auxiliary operations are candidates for unfolding since they are variants
-of existing logical concepts. The [simp] declarations try to move the attention
-of the casual user away from these auxiliary operations; if they expose problems
-in existing applications, they can be removed using [simp del] – the regular
-theory merge will make sure that this deviant setup will not persist in bigger
-developments. INCOMPATIBILITY.
-
-* ML bindings for theorems Ball_def, Bex_def, CollectD, CollectE, CollectI,
-Collect_conj_eq, Collect_mem_eq, IntD1, IntD2, IntE, IntI, Int_Collect, UNIV_I,
-UNIV_witness, UnE, UnI1, UnI2, ballE, ballI, bexCI, bexE, bexI, bex_triv, bspec,
-contra_subsetD, equalityCE, equalityD1, equalityD2, equalityE, equalityI,
-imageE, imageI, image_Un, image_insert, insert_commute, insert_iff,
-mem_Collect_eq, rangeE, rangeI, range_eqI, subsetCE, subsetD, subsetI,
-subset_refl, subset_trans, vimageD, vimageE, vimageI, vimageI2, vimage_Collect,
-vimage_Int, vimage_Un. INCOMPATIBILITY, use thm(s) antiquotation instead.
+The _def suffix for characteristic theorems is avoided to emphasize that
+these auxiliary operations are candidates for unfolding since they are
+variants of existing logical concepts. The [simp] declarations try to
+move the attention of the casual user away from these auxiliary
+operations; if they expose problems in existing applications, they can
+be removed using [simp del] – the regular theory merge will make sure
+that this deviant setup will not persist in bigger developments.
+INCOMPATIBILITY.
+
+* ML bindings for theorems Ball_def, Bex_def, CollectD, CollectE,
+CollectI, Collect_conj_eq, Collect_mem_eq, IntD1, IntD2, IntE, IntI,
+Int_Collect, UNIV_I, UNIV_witness, UnE, UnI1, UnI2, ballE, ballI, bexCI,
+bexE, bexI, bex_triv, bspec, contra_subsetD, equalityCE, equalityD1,
+equalityD2, equalityE, equalityI, imageE, imageI, image_Un,
+image_insert, insert_commute, insert_iff, mem_Collect_eq, rangeE,
+rangeI, range_eqI, subsetCE, subsetD, subsetI, subset_refl,
+subset_trans, vimageD, vimageE, vimageI, vimageI2, vimage_Collect,
+vimage_Int, vimage_Un. INCOMPATIBILITY, use thm(s) antiquotation
+instead.
* Clarified semantics for adding code equations:
* Code equations from preceding theories are superseded.
@@ -162,18 +164,18 @@
prepended.
INCOMPATIBILITY.
-* Normalization by evaluation (method "normalization", command value) could
-yield false positives due to incomplete handling of polymorphism in certain
-situations; this is now corrected.
+* Normalization by evaluation (method "normalization", command value)
+could yield false positives due to incomplete handling of polymorphism
+in certain situations; this is now corrected.
* Theory "HOL.Nat": Added Kleene's Fixed Point Theorem for lfp.
-* Theory "HOL-Library.Code_Target_Bit_Shifts" incorporated into HOL-Main.
-Minor INCOMPATIBILITY.
-
-* If "HOL-Library.Code_Target_Nat" is imported, bit operations on nat are
-implemented by bit operations on target-language integers.
-Minor INCOMPATIBILITY.
+* Theory "HOL-Library.Code_Target_Bit_Shifts" incorporated into
+HOL-Main. Minor INCOMPATIBILITY.
+
+* If theory "HOL-Library.Code_Target_Nat" is imported, bit operations on
+nat are implemented by bit operations on target-language integers. Minor
+INCOMPATIBILITY.
* Theory "HOL.Fun":
- Added lemmas.
@@ -314,6 +316,10 @@
*** ML ***
+* ML function "Raw_Simplifier.rewrite" has been renamed to
+"Raw_Simplifier.rewrite_wrt", to avoid clash with existing
+'Simplifier.rewrite'. INCOMPATIBILITY.
+
* Some old infix operations have been removed. INCOMPATIBILITY. The
subsequent replacements have slightly different syntactic precedence and
may require change of parentheses:
--- a/src/Pure/Build/build.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/Build/build.scala Wed Aug 06 17:39:03 2025 +0200
@@ -728,16 +728,18 @@
val thy_file = migrate_file(thy_file0)
val blobs =
- blobs_files0.map { name0 =>
- val name = migrate_file(name0)
+ blobs_files0.map { case (command_offset, name0) =>
+ val node_name = Document.Node.Name(migrate_file(name0))
+ val src_path = Path.explode(name0)
val file = read_source_file(name0)
val bytes = file.bytes
val text = decode(bytes.text)
val chunk = Symbol.Text_Chunk(text)
+ val content = Some((file.digest, chunk))
- Command.Blob(Document.Node.Name(name), Path.explode(name), Some((file.digest, chunk))) ->
- Document.Blobs.Item(bytes, text, chunk, changed = false)
+ Command.Blob(command_offset, node_name, src_path, content) ->
+ Document.Blobs.Item(bytes, text, chunk, command_offset = command_offset)
}
val thy_source = decode(read_source_file(thy_file0).bytes.text)
@@ -818,10 +820,9 @@
Build.read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
case None => progress.echo(thy_heading + " MISSING")
case Some(snapshot) =>
- val rendering = new Rendering(snapshot, options, session)
val messages =
- rendering.text_messages()
- .filter(message => progress.verbose || Protocol.is_exported(message.info))
+ Rendering.text_messages(snapshot,
+ filter = msg => progress.verbose || Protocol.is_exported(msg))
if (messages.nonEmpty) {
val line_document = Line.Document(snapshot.node.source)
val buffer = new mutable.ListBuffer[String]
--- a/src/Pure/Build/build_job.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/Build/build_job.scala Wed Aug 06 17:39:03 2025 +0200
@@ -150,20 +150,23 @@
def session_blobs(node_name: Document.Node.Name): List[(Command.Blob, Document.Blobs.Item)] =
session_background.base.theory_load_commands.get(node_name.theory) match {
case None => Nil
- case Some(spans) =>
+ case Some(load_commands) =>
val syntax = session_background.base.theory_syntax(node_name)
val master_dir = Path.explode(node_name.master_dir)
- for (span <- spans; file <- span.loaded_files(syntax).files)
- yield {
+ for {
+ (command_span, command_offset) <- load_commands
+ file <- command_span.loaded_files(syntax).files
+ } yield {
val src_path = Path.explode(file)
val blob_name = Document.Node.Name(File.symbolic_path(master_dir + src_path))
val bytes = session_sources(blob_name.node).bytes
val text = bytes.text
val chunk = Symbol.Text_Chunk(text)
+ val content = Some((SHA1.digest(bytes), chunk))
- Command.Blob(blob_name, src_path, Some((SHA1.digest(bytes), chunk))) ->
- Document.Blobs.Item(bytes, text, chunk, changed = false)
+ Command.Blob(command_offset, blob_name, src_path, content) ->
+ Document.Blobs.Item(bytes, text, chunk, command_offset = command_offset)
}
}
@@ -307,9 +310,11 @@
export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
}
- export_text(Export.FILES,
- cat_lines(snapshot.node_files.map(name => File.symbolic_path(name.path))),
- compress = false)
+ export_(Export.FILES,
+ {
+ import XML.Encode._
+ list(pair(int, string))(snapshot.node_export_files)
+ })
for ((blob_name, i) <- snapshot.node_files.tail.zipWithIndex) {
val xml = snapshot.switch(blob_name).xml_markup()
--- a/src/Pure/Build/export.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/Build/export.scala Wed Aug 06 17:39:03 2025 +0200
@@ -502,7 +502,7 @@
def db_source: Option[String] = {
val theory_context = session_context.theory(theory)
for {
- name <- theory_context.files0(permissive = true).headOption
+ (_, name) <- theory_context.files0(permissive = true).headOption
file <- get_source_file(name)
} yield Symbol.output(unicode_symbols, file.bytes.text)
}
@@ -549,13 +549,15 @@
case _ => None
}
- def files0(permissive: Boolean = false): List[String] =
- split_lines(apply(FILES, permissive = permissive).text)
+ def files0(permissive: Boolean = false): List[(Int, String)] = {
+ import XML.Decode._
+ list(pair(int, string))(apply(FILES, permissive = permissive).yxml())
+ }
- def files(permissive: Boolean = false): Option[(String, List[String])] =
+ def files(permissive: Boolean = false): Option[(String, List[(Int, String)])] =
files0(permissive = permissive) match {
case Nil => None
- case a :: bs => Some((a, bs))
+ case (_, a) :: bs => Some((a, bs))
}
override def toString: String = "Export.Theory_Context(" + quote(theory) + ")"
--- a/src/Pure/Build/resources.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/Build/resources.scala Wed Aug 06 17:39:03 2025 +0200
@@ -7,6 +7,7 @@
package isabelle
+import scala.collection.mutable
import scala.util.parsing.input.Reader
import java.io.{File => JFile}
@@ -32,6 +33,9 @@
def sessions_structure: Sessions.Structure = session_background.sessions_structure
def session_base: Sessions.Base = session_background.base
+ def loaded_theory(name: String): Boolean = session_base.loaded_theory(name)
+ def loaded_theory(name: Document.Node.Name): Boolean = session_base.loaded_theory(name)
+
override def toString: String = "Resources(" + session_base.print_body + ")"
@@ -85,14 +89,20 @@
def load_commands(
syntax: Outer_Syntax,
name: Document.Node.Name
- ) : () => List[Command_Span.Span] = {
+ ) : () => List[(Command_Span.Span, Symbol.Offset)] = {
val (is_utf8, raw_text) =
with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString))
() =>
{
if (syntax.has_load_commands(raw_text)) {
- val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text))
- syntax.parse_spans(text).filter(_.is_load_command(syntax))
+ val spans = syntax.parse_spans(Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text)))
+ val result = new mutable.ListBuffer[(Command_Span.Span, Symbol.Offset)]
+ var offset = 1
+ for (span <- spans) {
+ if (span.is_load_command(syntax)) { result += (span -> offset) }
+ offset += span.symbol_length
+ }
+ result.toList
}
else Nil
}
@@ -112,7 +122,7 @@
(file, theory) <- Thy_Header.ml_roots.iterator
node = append_path("~~/src/Pure", Path.explode(file))
node_name = Document.Node.Name(node, theory = theory)
- name <- loaded_files(syntax, node_name, load_commands(syntax, node_name)()).iterator
+ name <- loaded_files(syntax, node_name, load_commands(syntax, node_name)().map(_._1)).iterator
} yield name).toList
def global_theory(theory: String): Boolean =
@@ -144,7 +154,7 @@
if (literal_import && !Url.is_base_name(s)) {
error("Bad import of theory from other session via file-path: " + quote(s))
}
- if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+ if (loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
else {
find_theory_node(theory) match {
case Some(node_name) => node_name
@@ -236,7 +246,7 @@
def undefined_blobs(version: Document.Version): List[Document.Node.Name] =
(for {
(node_name, node) <- version.nodes.iterator
- if !session_base.loaded_theory(node_name)
+ if !loaded_theory(node_name)
cmd <- node.load_commands.iterator
name <- cmd.blobs_undefined.iterator
} yield name).toList
@@ -295,7 +305,7 @@
if (seen.isDefinedAt(name)) this
else {
val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct))
- if (session_base.loaded_theory(name)) dependencies1
+ if (loaded_theory(name)) dependencies1
else {
try {
if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators))
@@ -372,9 +382,9 @@
def get_syntax(name: Document.Node.Name): Outer_Syntax =
loaded_theories.get_node(name.theory)
- lazy val load_commands: List[(Document.Node.Name, List[Command_Span.Span])] =
+ lazy val load_commands: List[(Document.Node.Name, List[(Command_Span.Span, Symbol.Offset)])] =
theories.zip(
- Par_List.map((e: () => List[Command_Span.Span]) => e(),
+ Par_List.map((e: () => List[(Command_Span.Span, Symbol.Offset)]) => e(),
theories.map(name => resources.load_commands(get_syntax(name), name))))
.filter(p => p._2.nonEmpty)
@@ -391,8 +401,8 @@
def loaded_files: List[Document.Node.Name] =
for {
- (name, spans) <- load_commands
- file <- loaded_files(name, spans)._2
+ (name, cmds) <- load_commands
+ file <- loaded_files(name, cmds.map(_._1))._2
} yield file
def imported_files: List[Path] = {
--- a/src/Pure/Build/sessions.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/Build/sessions.scala Wed Aug 06 17:39:03 2025 +0200
@@ -102,7 +102,7 @@
document_theories: List[Document.Node.Name] = Nil,
loaded_theories: Graph[String, Outer_Syntax] = Graph.string, // cumulative imports
used_theories: List[(Document.Node.Name, Options)] = Nil, // new imports
- theory_load_commands: Map[String, List[Command_Span.Span]] = Map.empty,
+ theory_load_commands: Map[String, List[(Command_Span.Span, Symbol.Offset)]] = Map.empty,
known_theories: Map[String, Document.Node.Entry] = Map.empty,
known_loaded_files: Map[String, List[Path]] = Map.empty,
overall_syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -301,11 +301,11 @@
catch { case ERROR(msg) => (Nil, List(msg)) }
val theory_load_commands =
- (for ((name, span) <- load_commands.iterator) yield name.theory -> span).toMap
+ (for ((name, cmd) <- load_commands.iterator) yield name.theory -> cmd).toMap
val loaded_files: List[(String, List[Path])] =
- for ((name, spans) <- load_commands) yield {
- val (theory, files) = dependencies.loaded_files(name, spans)
+ for ((name, cmds) <- load_commands) yield {
+ val (theory, files) = dependencies.loaded_files(name, cmds.map(_._1))
theory -> files.map(file => Path.explode(file.node))
}
--- a/src/Pure/Isar/toplevel.ML Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Aug 06 17:39:03 2025 +0200
@@ -81,7 +81,6 @@
val skip_proof_close: transition -> transition
val exec_id: Document_ID.exec -> transition -> transition
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
- val transition: bool -> transition -> state -> state * (exn * string) option
val command_errors: bool -> transition -> state -> Runtime.error list * state option
val command_exception: bool -> transition -> state -> state
val reset_theory: state -> state option
@@ -612,13 +611,16 @@
Position.setmp_thread_data (Position.label (Long_Name.qualify Markup.commandN name) pos) f x;
-(* apply transitions *)
+(* command transitions *)
local
-fun show_state (st', opt_err) =
+fun show_state tr (st', opt_err) =
let
- val enabled = is_none opt_err andalso Options.default_bool \<^system_option>\<open>show_states\<close>;
+ val enabled =
+ not (is_ignored tr) andalso
+ is_none opt_err andalso
+ Options.default_bool \<^system_option>\<open>show_states\<close>;
val opt_err' =
if enabled then
(case Exn.capture (Output.state o Pretty.strings_of o Pretty.chunks o pretty_state) st' of
@@ -631,11 +633,9 @@
setmp_thread_position tr
(Timing.protocol (name_of tr) (pos_of tr) (apply_capture int name markers trans)
##> Option.map (fn Runtime.UNDEF => ERROR (type_error tr) | exn => exn)
- #> show_state);
+ #> show_state tr);
-in
-
-fun transition int tr st =
+fun command_transition int tr st =
let
val (st', opt_err) =
Context.setmp_generic_context (try (Context.Proof o presentation_context0) st)
@@ -645,18 +645,15 @@
| exn => (Runtime.exn_context (try context_of st) exn, at_command tr));
in (st', opt_err') end;
-end;
-
-
-(* managed commands *)
+in
fun command_errors int tr st =
- (case transition int tr st of
+ (case command_transition int tr st of
(st', NONE) => ([], SOME st')
| (_, SOME (exn, _)) => (Runtime.exn_messages exn, NONE));
fun command_exception int tr st =
- (case transition int tr st of
+ (case command_transition int tr st of
(st', NONE) => st'
| (_, SOME (exn, info)) =>
if Exn.is_interrupt_proper exn then Exn.reraise exn
@@ -664,6 +661,8 @@
val command = command_exception false;
+end;
+
(* reset state *)
--- a/src/Pure/PIDE/command.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/command.scala Wed Aug 06 17:39:03 2025 +0200
@@ -15,6 +15,7 @@
/* blobs */
sealed case class Blob(
+ command_offset: Symbol.Offset,
name: Document.Node.Name,
src_path: Path,
content: Option[(SHA1.Digest, Symbol.Text_Chunk)]
@@ -454,7 +455,7 @@
val src_path = Path.explode(file)
val name = Document.Node.Name(resources.append_path(node_name.master_dir, src_path))
val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
- Blob(name, src_path, content)
+ Blob(0, name, src_path, content)
}).user_error)
Blobs_Info(blobs, index = loaded_files.index)
}
@@ -496,6 +497,9 @@
def blobs_names: List[Document.Node.Name] =
for (case Exn.Res(blob) <- blobs) yield blob.name
+ def blobs_files: List[(Symbol.Offset, Document.Node.Name)] =
+ for (case Exn.Res(blob) <- blobs) yield (blob.command_offset, blob.name)
+
def blobs_undefined: List[Document.Node.Name] =
for (case Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name
--- a/src/Pure/PIDE/command_span.ML Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/command_span.ML Wed Aug 06 17:39:03 2025 +0200
@@ -11,12 +11,14 @@
datatype span = Span of kind * Token.T list
val kind: span -> kind
val content: span -> Token.T list
+ val range: span -> Position.range
val symbol_length: span -> int option
val eof: span
val is_eof: span -> bool
val stopper: span Scan.stopper
val adjust_offsets_kind: (int -> int option) -> kind -> kind
val adjust_offsets: (int -> int option) -> span -> span
+ val command_ranges: span list -> Position.range list
end;
structure Command_Span: COMMAND_SPAN =
@@ -34,7 +36,8 @@
fun kind (Span (k, _)) = k;
fun content (Span (_, toks)) = toks;
-val symbol_length = Position.distance_of o Token.range_of o content;
+val range = Token.range_of o content;
+val symbol_length = Position.distance_of o range;
(* stopper *)
@@ -57,4 +60,24 @@
fun adjust_offsets adjust (Span (k, toks)) =
Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks);
+
+(* command ranges, including trailing non-commands (whitespace etc.) *)
+
+fun command_ranges spans =
+ let
+ fun ranges NONE [] result = rev result
+ | ranges (SOME pos) [] result =
+ let val end_pos = #2 (range (List.last spans))
+ in rev (Position.range (pos, end_pos) :: result) end
+ | ranges start_pos (span :: rest) result =
+ (case (start_pos, kind span) of
+ (NONE, Command_Span _) => ranges (SOME (#1 (range span))) rest result
+ | (SOME pos, Command_Span _) =>
+ let
+ val pos' = #1 (range span);
+ val result' = Position.range (pos, pos') :: result;
+ in ranges (SOME pos') rest result' end
+ | _ => ranges start_pos rest result);
+ in ranges NONE spans [] end;
+
end;
--- a/src/Pure/PIDE/command_span.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/command_span.scala Wed Aug 06 17:39:03 2025 +0200
@@ -102,6 +102,7 @@
def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content))
def length: Int = content.foldLeft(0)(_ + _.source.length)
+ def symbol_length: Symbol.Offset = content.foldLeft(0)(_ + _.symbol_length)
def compact_source: (String, Span) = {
val source = Token.implode(content)
--- a/src/Pure/PIDE/document.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/document.scala Wed Aug 06 17:39:03 2025 +0200
@@ -46,8 +46,14 @@
bytes: Bytes,
source: String,
chunk: Symbol.Text_Chunk,
- changed: Boolean
+ command_offset: Symbol.Offset = 0,
+ changed: Boolean = false
) {
+ override def toString: String =
+ "Blobs.Item(bytes = " + bytes.size + ", source = " + source.length +
+ if_proper(command_offset > 0, ", command_offset = " + command_offset) +
+ if_proper(changed, ", changed = true") + ")"
+
def source_wellformed: Boolean = bytes.wellformed_text.nonEmpty
def unchanged: Item = if (changed) copy(changed = false) else this
}
@@ -588,6 +594,10 @@
def node_files: List[Node.Name] =
node_name :: node.load_commands.flatMap(_.blobs_names)
+ def node_export_files: List[(Symbol.Offset, String)] =
+ for ((i, name) <- (0, node_name) :: node.load_commands.flatMap(_.blobs_files))
+ yield (i, File.symbolic_path(name.path))
+
def node_consolidated(name: Node.Name): Boolean =
state.node_consolidated(version, name)
@@ -597,6 +607,25 @@
case None => false
}
+ def loaded_theory_command(caret_offset: Text.Offset): Option[(Command, Text.Range)] =
+ if (node_name.is_theory) {
+ node.commands.get_after(None) match {
+ case Some(command) if command.span.is_theory =>
+ Some(command -> command_range(Text.Range(caret_offset)).getOrElse(Text.Range.offside))
+ case _ => None
+ }
+ }
+ else {
+ for {
+ command <- version.nodes.commands_loading(node_name).find(_.span.is_theory)
+ (symbol_offset, _) <- command.blobs_files.find({ case (_, name) => node_name == name })
+ } yield {
+ val chunk_offset = command.chunk.decode(symbol_offset)
+ val command_range = switch(command.node_name).command_range(Text.Range(chunk_offset))
+ command -> command_range.getOrElse(Text.Range.offside)
+ }
+ }
+
/* pending edits */
@@ -816,6 +845,7 @@
/* command spans --- according to PIDE markup */
+ // Text.Info: core range
def command_spans(range: Text.Range = Text.Range.full): List[Text.Info[Markup.Command_Span.Args]] =
select(range, Markup.Elements(Markup.COMMAND_SPAN), _ =>
{
@@ -823,6 +853,13 @@
Some(Text.Info(range, args))
case _ => None
}).map(_.info)
+
+ // Text.Range: full source with trailing whitespace etc.
+ def command_range(caret_range: Text.Range): Option[Text.Range] =
+ select(caret_range, Markup.Elements(Markup.COMMAND_RANGE), _ =>
+ {
+ case Text.Info(range, _) => Some(range)
+ }).headOption.map(_.info)
}
@@ -862,7 +899,7 @@
case None =>
List(
Node.Deps(
- if (session.resources.session_base.loaded_theory(node_name)) {
+ if (session.resources.loaded_theory(node_name)) {
node_header.append_errors(
List("Cannot update finished theory " + quote(node_name.theory)))
}
--- a/src/Pure/PIDE/document_editor.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/document_editor.scala Wed Aug 06 17:39:03 2025 +0200
@@ -141,7 +141,7 @@
else {
val snapshot = pide_session.snapshot()
def document_ready(theory: String): Boolean =
- pide_session.resources.session_base.loaded_theory(theory) ||
+ pide_session.resources.loaded_theory(theory) ||
snapshot.theory_consolidated(theory)
if (snapshot.is_outdated || !selection.forall(document_ready)) None
else Some(snapshot)
--- a/src/Pure/PIDE/document_info.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/document_info.scala Wed Aug 06 17:39:03 2025 +0200
@@ -103,7 +103,7 @@
Theory(theory_name,
static_session = sessions_structure.theory_qualifier(theory_name),
dynamic_session = session_name,
- files = files,
+ files = files.map(_._2),
entities = theory_export.entity_iterator.toList,
others = theory_export.others.keySet.toList)
Some(theory)
--- a/src/Pure/PIDE/document_status.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala Wed Aug 06 17:39:03 2025 +0200
@@ -275,7 +275,7 @@
val update_iterator =
for {
name <- domain.getOrElse(nodes1.domain).iterator
- if !Resources.hidden_node(name) && !resources.session_base.loaded_theory(name)
+ if !Resources.hidden_node(name) && !resources.loaded_theory(name)
st = Document_Status.Node_Status.make(state, version, name)
if !rep.isDefinedAt(name) || rep(name) != st
} yield (name -> st)
--- a/src/Pure/PIDE/editor.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/editor.scala Wed Aug 06 17:39:03 2025 +0200
@@ -7,6 +7,21 @@
package isabelle
+object Editor {
+ /* output messages */
+
+ object Output {
+ val none: Output = Output(defined = false)
+ val init: Output = Output()
+ }
+
+ sealed case class Output(
+ results: Command.Results = Command.Results.empty,
+ messages: List[XML.Elem] = Nil,
+ defined: Boolean = true
+ )
+}
+
abstract class Editor[Context] {
/* PIDE session and document model */
@@ -89,6 +104,48 @@
def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
+ /* output messages */
+
+ def output_state(): Boolean
+
+ def output(
+ snapshot: Document.Snapshot,
+ caret_offset: Text.Offset,
+ restriction: Option[Set[Command]] = None
+ ): Editor.Output = {
+ if (snapshot.is_outdated) Editor.Output.none
+ else {
+ val thy_command_range = snapshot.loaded_theory_command(caret_offset)
+ val thy_command = thy_command_range.map(_._1)
+
+ def filter(msg: XML.Elem): Boolean =
+ (for {
+ (command, command_range) <- thy_command_range
+ msg_offset <- Position.Offset.unapply(msg.markup.properties)
+ } yield command_range.contains(command.chunk.decode(msg_offset))) getOrElse true
+
+ thy_command orElse snapshot.current_command(snapshot.node_name, caret_offset) match {
+ case None => Editor.Output.init
+ case Some(command) =>
+ if (thy_command.isDefined || restriction.isEmpty || restriction.get.contains(command)) {
+ val results = snapshot.command_results(command)
+ val messages = {
+ val (states, other) = {
+ List.from(
+ for ((_, msg) <- results.iterator if !Protocol.is_result(msg) && filter(msg))
+ yield msg).partition(Protocol.is_state)
+ }
+ val (urgent, regular) = other.partition(Protocol.is_urgent)
+ urgent ::: (if (output_state()) states else Nil) ::: regular
+ }
+ Editor.Output(results = results, messages = messages)
+ }
+ else Editor.Output.none
+ }
+ }
+ }
+
+
/* overlays */
def node_overlays(name: Document.Node.Name): Document.Node.Overlays
--- a/src/Pure/PIDE/headless.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/headless.scala Wed Aug 06 17:39:03 2025 +0200
@@ -54,9 +54,6 @@
override def resources: Headless.Resources = _resources
- private def loaded_theory(name: Document.Node.Name): Boolean =
- resources.session_base.loaded_theory(name.theory)
-
/* options */
@@ -94,7 +91,7 @@
def finished: Load_State = Load_State(Nil, Nil, Space.zero)
def count_file(name: Document.Node.Name): Long =
- if (loaded_theory(name)) 0 else File.size(name.path)
+ if (resources.loaded_theory(name)) 0 else File.size(name.path)
}
private case class Load_State(
@@ -209,7 +206,7 @@
version: Document.Version,
name: Document.Node.Name
): Boolean = {
- loaded_theory(name) ||
+ resources.loaded_theory(name) ||
nodes_status.quasi_consolidated(name) ||
(if (commit.isDefined) already_committed.isDefinedAt(name)
else state.node_consolidated(version, name))
@@ -229,7 +226,7 @@
case (committed, name) =>
def parents_committed: Boolean =
version.nodes(name).header.imports.forall(parent =>
- loaded_theory(parent) || committed.isDefinedAt(parent))
+ resources.loaded_theory(parent) || committed.isDefinedAt(parent))
if (!committed.isDefinedAt(name) && parents_committed &&
state.node_consolidated(version, name)) {
val snapshot = stable_snapshot(state, version, name)
@@ -242,7 +239,7 @@
}
def committed(name: Document.Node.Name): Boolean =
- loaded_theory(name) || st1.already_committed.isDefinedAt(name)
+ resources.loaded_theory(name) || st1.already_committed.isDefinedAt(name)
val (load_theories0, load_state1) =
load_state.next(dep_graph, consolidated(state, version, _))
@@ -260,7 +257,7 @@
): Option[List[(Document.Node.Name, Document_Status.Node_Status)]] = {
input match {
case name :: rest =>
- if (loaded_theory(name)) make_nodes(rest, output)
+ if (resources.loaded_theory(name)) make_nodes(rest, output)
else {
val status = Document_Status.Node_Status.make(state, version, name)
val ok = if (commit.isDefined) committed(name) else status.consolidated
--- a/src/Pure/PIDE/markup.ML Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/markup.ML Wed Aug 06 17:39:03 2025 +0200
@@ -183,6 +183,7 @@
val inputN: string val input: bool -> Properties.T -> T
val command_keywordN: string val command_keyword: T
val command_spanN: string val command_span: {name: string, kind: string, is_begin: bool} -> T
+ val command_rangeN: string val command_range: T
val commandN: string val command_properties: T -> T
val keywordN: string val keyword_properties: T -> T
val stringN: string val string: T
@@ -664,6 +665,8 @@
fun command_span {name, kind, is_begin} : T =
(command_spanN, name_proper name @ kind_proper kind @ Properties.make_bool is_beginN is_begin);
+val (command_rangeN, command_range) = markup_elem "command_range";
+
val commandN = "command"; val command_properties = properties [(kindN, commandN)];
val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
--- a/src/Pure/PIDE/markup.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/markup.scala Wed Aug 06 17:39:03 2025 +0200
@@ -464,6 +464,8 @@
else None
}
+ val COMMAND_RANGE = "command_range"
+
val COMMAND = "command"
val KEYWORD = "keyword"
val KEYWORD1 = "keyword1"
--- a/src/Pure/PIDE/protocol.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Aug 06 17:39:03 2025 +0200
@@ -346,7 +346,7 @@
val blobs_xml: XML.Body = {
val encode_blob: T[Exn.Result[Command.Blob]] =
variant(List(
- { case Exn.Res(Command.Blob(a, b, c)) =>
+ { case Exn.Res(Command.Blob(_, a, b, c)) =>
(Nil, triple(string, string, option(string))(
(a.node, b.implode, c.map(p => p._1.toString)))) },
{ case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
--- a/src/Pure/PIDE/rendering.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala Wed Aug 06 17:39:03 2025 +0200
@@ -95,13 +95,37 @@
legacy_pri -> Color.legacy_message,
error_pri -> Color.error_message)
- def output_messages(results: Command.Results, output_state: Boolean): List[XML.Elem] = {
- val (states, other) =
- results.iterator.map(_._2).filterNot(Protocol.is_result).toList
- .partition(Protocol.is_state)
- val (urgent, regular) = other.partition(Protocol.is_urgent)
+
+ /* text messages */
- urgent ::: (if (output_state) states else Nil) ::: regular
+ def text_messages(
+ snapshot: Document.Snapshot,
+ range: Text.Range = Text.Range.full,
+ filter: XML.Elem => Boolean = _ => true
+ ): List[Text.Info[XML.Elem]] = {
+ val results =
+ snapshot.cumulate[Vector[Command.Results.Entry]](
+ range, Vector.empty, message_elements, command_states =>
+ {
+ case (res, Text.Info(_, elem)) =>
+ if (filter(elem)) {
+ Command.State.get_result_proper(command_states, elem.markup.properties)
+ .map(res :+ _)
+ }
+ else None
+ })
+
+ var seen_serials = Set.empty[Long]
+ def seen(i: Long): Boolean = {
+ val b = seen_serials(i)
+ seen_serials += i
+ b
+ }
+ List.from(
+ for {
+ Text.Info(range, entries) <- results.iterator
+ (i, elem) <- entries.iterator if !seen(i)
+ } yield Text.Info(range, elem))
}
@@ -570,28 +594,6 @@
} yield Text.Info(r, color)
}
- def text_messages(range: Text.Range = Text.Range.full): List[Text.Info[XML.Elem]] = {
- val results =
- snapshot.cumulate[Vector[Command.Results.Entry]](
- range, Vector.empty, Rendering.message_elements, command_states =>
- {
- case (res, Text.Info(_, elem)) =>
- Command.State.get_result_proper(command_states, elem.markup.properties)
- .map(res :+ _)
- })
-
- var seen_serials = Set.empty[Long]
- def seen(i: Long): Boolean = {
- val b = seen_serials(i)
- seen_serials += i
- b
- }
- for {
- Text.Info(range, entries) <- results
- (i, elem) <- entries if !seen(i)
- } yield Text.Info(range, elem)
- }
-
/* markup structure */
--- a/src/Pure/PIDE/session.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/session.scala Wed Aug 06 17:39:03 2025 +0200
@@ -130,12 +130,19 @@
override def session_options: Options = options
override def resources: Resources = Resources.bootstrap
}
+
+
+ /* read_theory cache */
+
+ sealed case class Read_Theory_Key(name: String, unicode_symbols: Boolean)
}
abstract class Session extends Document.Session {
session =>
+ override def toString: String = resources.session_base.session_name
+
def session_options: Options
def resources: Resources
@@ -155,23 +162,25 @@
store, resources.session_background, document_snapshot = document_snapshot)
}
- private val read_theory_cache = new WeakHashMap[String, WeakReference[Command]]
+ private val read_theory_cache =
+ new WeakHashMap[Session.Read_Theory_Key, WeakReference[Document.Snapshot]]
- def read_theory(name: String): Command =
+ def read_theory(name: String, unicode_symbols: Boolean = false): Document.Snapshot =
read_theory_cache.synchronized {
- Option(read_theory_cache.get(name)).map(_.get) match {
- case Some(command: Command) => command
+ val key = Session.Read_Theory_Key(name, unicode_symbols)
+ Option(read_theory_cache.get(key)).map(_.get) match {
+ case Some(snapshot: Document.Snapshot) => snapshot
case _ =>
- val snapshot =
+ val maybe_snapshot =
using(open_session_context()) { session_context =>
Build.read_theory(session_context.theory(name),
- unicode_symbols = true,
+ unicode_symbols = unicode_symbols,
migrate_file = (a: String) => session.resources.append_path("", Path.explode(a)))
}
- snapshot.map(_.snippet_commands) match {
- case Some(List(command)) =>
- read_theory_cache.put(name, new WeakReference(command))
- command
+ maybe_snapshot.map(_.snippet_commands) match {
+ case Some(List(_)) =>
+ read_theory_cache.put(key, new WeakReference(maybe_snapshot.get))
+ maybe_snapshot.get
case _ => error("Failed to load theory " + quote(name) + " from session database")
}
}
@@ -672,7 +681,7 @@
case Some(version) =>
val consolidate =
version.nodes.descendants(consolidation.flush().toList).filter { name =>
- !resources.session_base.loaded_theory(name) &&
+ !resources.loaded_theory(name) &&
!state.node_consolidated(version, name) &&
state.node_maybe_consolidated(version, name)
}
--- a/src/Pure/PIDE/text.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/PIDE/text.scala Wed Aug 06 17:39:03 2025 +0200
@@ -152,7 +152,7 @@
final class Edit private(val is_insert: Boolean, val start: Offset, val text: String) {
override def toString: String =
- (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
+ (if (is_insert) "Insert(" else "Remove(") + (start, text.length).toString + ")"
/* transform offsets */
--- a/src/Pure/ROOT.ML Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/ROOT.ML Wed Aug 06 17:39:03 2025 +0200
@@ -1,6 +1,6 @@
(* Title: Pure/ROOT.ML
Author: Makarius
- UUID: a83d12be-3568-49ab-9484-a84de5cee2bf
+ UUID: 2dddcab9-800b-4158-b53a-f20f73aa7663
Main entry point for the Isabelle/Pure bootstrap process.
--- a/src/Pure/Thy/thy_info.ML Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Aug 06 17:39:03 2025 +0200
@@ -300,6 +300,8 @@
val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
val elements = Thy_Element.parse_elements keywords spans;
+ val command_ranges =
+ Command_Span.command_ranges spans |> map (fn (pos, _) => (pos, Markup.command_range));
val text_id = Position.copy_id text_pos Position.none;
@@ -307,6 +309,8 @@
fun excursion () =
let
+ val _ = Position.setmp_thread_data text_id (fn () => Position.reports command_ranges) ();
+
fun element_result span_elem (st, _) =
let
fun prepare span =
--- a/src/Pure/Thy/thy_syntax.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Aug 06 17:39:03 2025 +0200
@@ -67,7 +67,7 @@
/** header edits: graph structure and outer syntax **/
private def header_edits(
- session_base: Sessions.Base,
+ resources: Resources,
previous: Document.Version,
edits: List[Document.Edit_Text]
): (List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) = {
@@ -76,7 +76,7 @@
val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
edits foreach {
- case (name, Document.Node.Deps(header)) if !session_base.loaded_theory(name) =>
+ case (name, Document.Node.Deps(header)) if !resources.loaded_theory(name) =>
val node = nodes(name)
val update_header =
node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header
@@ -102,9 +102,9 @@
val header = node.header
val imports_syntax =
if (header.imports.nonEmpty) {
- Outer_Syntax.merge(header.imports.map(session_base.node_syntax(nodes, _)))
+ Outer_Syntax.merge(header.imports.map(resources.session_base.node_syntax(nodes, _)))
}
- else session_base.overall_syntax
+ else resources.session_base.overall_syntax
Some(imports_syntax + header)
}
nodes += (name -> node.update_syntax(syntax))
@@ -160,34 +160,43 @@
require(node_name.is_theory)
val theory = node_name.theory
- Exn.capture(session.read_theory(theory)) match {
- case Exn.Res(command) =>
- val thy_changed =
- if (node.source.isEmpty || node.source == command.source) Nil
- else List(node_name.node)
- val blobs_changed =
- for {
- case Exn.Res(blob) <- command.blobs
- (digest, _) <- blob.content
- doc_blob <- doc_blobs.get(blob.name)
- if digest != doc_blob.bytes.sha1_digest
- } yield blob.name.node
+ val node_source = node.source
+ val unicode_symbols = Symbol.decode(node_source) == node_source
- val changed = thy_changed ::: blobs_changed
- val command1 =
- if (changed.isEmpty) command
+ Exn.capture(session.read_theory(theory, unicode_symbols = unicode_symbols)) match {
+ case Exn.Res(snapshot) =>
+ val command = snapshot.snippet_commands.head
+ val node_commands =
+ if (node.is_empty) Linear_Set.empty
else {
- val node_range = Text.Range(0, Symbol.length(node.source))
- val msg =
- XML.Elem(Markup.Bad(Document_ID.make()),
- XML.string("Changed sources for loaded theory " + quote(theory) +
- ":\n" + cat_lines(changed.map(a => " " + quote(a)))))
- Command.unparsed(node.source, theory = true, id = command.id, node_name = node_name,
- blobs_info = command.blobs_info,
- markups = Command.Markups.empty.add(Text.Info(node_range, msg)))
+ val thy_changed = if (node_source == command.source) Nil else List(node_name.node)
+ val blobs_changed =
+ List.from(
+ for {
+ blob_name <- command.blobs_names.iterator
+ blob_node = snapshot.version.nodes(blob_name)
+ doc_blob <- doc_blobs.get(blob_name)
+ if blob_node.source != doc_blob.source
+ } yield blob_name.node)
+
+ val changed = thy_changed ::: blobs_changed
+ val command1 =
+ if (changed.isEmpty) command
+ else {
+ val node_range = Text.Range(0, Symbol.length(node.source))
+ val msg =
+ XML.Elem(Markup.Bad(Document_ID.make()),
+ XML.string("Changed sources for loaded theory " + quote(theory) +
+ ":\n" + cat_lines(changed.map(a => " " + quote(a)))))
+ Command.unparsed(node.source, theory = true, id = command.id, node_name = node_name,
+ blobs_info = command.blobs_info,
+ markups = Command.Markups.empty.add(Text.Info(node_range, msg)))
+ }
+
+ Linear_Set(command1)
}
- node.update_commands(Linear_Set(command1))
+ node.update_commands(node_commands)
case Exn.Exn(exn) =>
session.system_output(Output.error_message_text(Exn.print(exn)))
@@ -219,7 +228,7 @@
first: Command,
last: Command
): Linear_Set[Command] = {
- require(!resources.session_base.loaded_theory(node_name))
+ require(!resources.loaded_theory(node_name))
val cmds0 = commands.iterator(first, last).toList
val blobs_spans0 =
@@ -268,8 +277,6 @@
node: Document.Node,
edit: Document.Edit_Text
): Document.Node = {
- val session_base = resources.session_base
-
/* recover command spans after edits */
// FIXME somewhat slow
def recover_spans(
@@ -302,7 +309,7 @@
if (name.is_theory) {
val commands1 = edit_text(text_edits, node.commands)
val commands2 =
- if (session_base.loaded_theory(name)) commands1
+ if (resources.loaded_theory(name)) commands1
else recover_spans(name, node.perspective.visible, commands1)
node.update_commands(commands2)
}
@@ -310,7 +317,7 @@
case (_, Document.Node.Deps(_)) => node
- case (name, Document.Node.Perspective(_, _, _)) if session_base.loaded_theory(name) => node
+ case (name, Document.Node.Perspective(_, _, _)) if resources.loaded_theory(name) => node
case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
@@ -355,16 +362,15 @@
consolidate: List[Document.Node.Name]
): Session.Change = {
val resources = session.resources
- val session_base = resources.session_base
val reparse_limit = session.reparse_limit
- val (syntax_changed, nodes0, doc_edits0) = header_edits(session_base, previous, edits)
+ val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
def get_blob(name: Document.Node.Name): Option[Document.Blobs.Item] =
doc_blobs.get(name) orElse previous.nodes(name).get_blob
def can_import(name: Document.Node.Name): Boolean =
- session_base.loaded_theory(name) || nodes0(name).has_header
+ resources.loaded_theory(name) || nodes0(name).has_header
val (doc_edits, version) =
if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
@@ -387,11 +393,11 @@
node_edits foreach {
case (name, edits) =>
val node = nodes(name)
- val syntax = session_base.node_syntax(nodes, name)
+ val syntax = resources.session_base.node_syntax(nodes, name)
val commands = node.commands
val node1 =
- if (!session_base.loaded_theory(name) && reparse_set(name) && commands.nonEmpty) {
+ if (!resources.loaded_theory(name) && reparse_set(name) && commands.nonEmpty) {
node.update_commands(
reparse_spans(resources, syntax, get_blob, can_import, name,
commands, commands.head, commands.last))
@@ -401,7 +407,7 @@
edits.foldLeft(node1)(
text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
val node3 =
- if (session_base.loaded_theory(name)) {
+ if (resources.loaded_theory(name)) {
reload_theory(session, doc_blobs, name, node2)
}
else if (reparse_set(name)) {
@@ -414,7 +420,7 @@
doc_edits += (name -> node3.perspective)
}
- if (!session_base.loaded_theory(name)) {
+ if (!resources.loaded_theory(name)) {
doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))
}
--- a/src/Pure/Tools/dump.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Pure/Tools/dump.scala Wed Aug 06 17:39:03 2025 +0200
@@ -232,7 +232,7 @@
session_name <-
deps.sessions_structure.build_graph.restrict(selected_sessions.toSet).topological_order
(name, theory_options) <- deps(session_name).used_theories
- if !resources.session_base.loaded_theory(name.theory)
+ if !resources.loaded_theory(name)
if {
def warn(msg: String): Unit =
progress.echo_warning("Skipping theory " + name + " (" + msg + ")")
--- a/src/Tools/VSCode/src/dynamic_output.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala Wed Aug 06 17:39:03 2025 +0200
@@ -19,26 +19,15 @@
def pretty_panel: Pretty_Text_Panel =
pretty_panel_.value.getOrElse(error("No Pretty Panel for Dynamic Output"))
- private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = {
+ private def handle_update(restriction: Option[Set[Command]] = None): Unit = {
val output =
server.resources.get_caret() match {
- case None => Some(Nil)
+ case None => Editor.Output.init
case Some(caret) =>
val snapshot = server.resources.snapshot(caret.model)
- snapshot.current_command(caret.node_name, caret.offset) match {
- case None => Some(Nil)
- case Some(command) =>
- if (restriction.isEmpty || restriction.get.contains(command)) {
- val output_state = server.resources.options.bool("editor_output_state")
- Some(Rendering.output_messages(snapshot.command_results(command), output_state))
- } else None
- }
+ server.editor.output(snapshot, caret.offset)
}
-
- output match {
- case None =>
- case Some(output) => pretty_panel.refresh(output)
- }
+ if (output.defined) pretty_panel.refresh(output.messages)
}
@@ -47,10 +36,10 @@
private val main =
Session.Consumer[Any](getClass.getName) {
case changed: Session.Commands_Changed =>
- handle_update(if (changed.assignment) None else Some(changed.commands))
+ handle_update(restriction = if (changed.assignment) None else Some(changed.commands))
case Session.Caret_Focus =>
- handle_update(None)
+ handle_update()
}
def init(): Unit = {
@@ -61,7 +50,7 @@
server.session,
server.channel,
LSP.Dynamic_Output.apply)))
- handle_update(None)
+ handle_update()
}
def exit(): Unit = {
--- a/src/Tools/VSCode/src/language_server.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Wed Aug 06 17:39:03 2025 +0200
@@ -579,14 +579,20 @@
def current_command(snapshot: Document.Snapshot): Option[Command] = {
resources.get_caret() match {
- case Some(caret) => snapshot.current_command(caret.node_name, caret.offset)
- case None => None
+ case Some(caret) if snapshot.loaded_theory_command(caret.offset).isEmpty =>
+ snapshot.current_command(caret.node_name, caret.offset)
+ case _ => None
}
}
override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] =
current_command(snapshot)
+ /* output messages */
+
+ override def output_state(): Boolean = resources.options.bool("editor_output_state")
+
+
/* overlays */
override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
--- a/src/Tools/VSCode/src/pretty_text_panel.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala Wed Aug 06 17:39:03 2025 +0200
@@ -43,52 +43,46 @@
Pretty.formatted(Pretty.separate(output), margin = margin, metric = Symbol.Metric)
if (formatted != current_formatted) {
+ val message = {
+ if (resources.html_output) {
+ val node_context =
+ new Browser_Info.Node_Context {
+ override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
+ for {
+ thy_file <- Position.Def_File.unapply(props)
+ def_line <- Position.Def_Line.unapply(props)
+ platform_path <- session.store.source_file(thy_file)
+ uri = File.uri(Path.explode(File.standard_path(platform_path)).absolute_file)
+ } yield HTML.link(uri.toString + "#" + def_line, body)
+ }
+ val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
+ val html = node_context.make_html(elements, formatted)
+ output_json(HTML.source(html).toString, None)
+ }
+ else {
+ val converted = resources.output_text_xml(formatted)
+ val converted_tree = Markup_Tree.from_XML(converted)
+ val converted_text = XML.content(converted)
+
+ val document = Line.Document(converted_text)
+ val decorations =
+ converted_tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements,
+ { case (_, m) => Some(Some(m.info.markup)) }
+ ).flatMap(info =>
+ info.info match {
+ case Some(markup) =>
+ val range = document.range(info.range)
+ Some((range, "text_" + Rendering.get_text_color(markup).get.toString))
+ case None => None
+ }
+ ).groupMap(_._2)(e => LSP.Decoration_Options(e._1, Nil)).toList
+
+ output_json(converted_text, Some(LSP.Decoration(decorations)))
+ }
+ }
+ channel.write(message)
current_output = output
current_formatted = formatted
-
- if (resources.html_output) {
- val node_context =
- new Browser_Info.Node_Context {
- override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
- for {
- thy_file <- Position.Def_File.unapply(props)
- def_line <- Position.Def_Line.unapply(props)
- platform_path <- session.store.source_file(thy_file)
- uri = File.uri(Path.explode(File.standard_path(platform_path)).absolute_file)
- } yield HTML.link(uri.toString + "#" + def_line, body)
- }
- val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
- val html = node_context.make_html(elements, formatted)
- val message = output_json(HTML.source(html).toString, None)
- channel.write(message)
- }
- else {
- def convert_symbols(body: XML.Body): XML.Body =
- body.map {
- case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body))
- case XML.Text(content) => XML.Text(resources.output_text(content))
- }
-
- val converted = convert_symbols(formatted)
-
- val tree = Markup_Tree.from_XML(converted)
- val text = XML.content(converted)
-
- val document = Line.Document(text)
- val decorations =
- tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements,
- { case (_, m) => Some(Some(m.info.markup)) }
- ).flatMap(info =>
- info.info match {
- case Some(markup) =>
- val range = document.range(info.range)
- Some((range, "text_" + Rendering.get_text_color(markup).get.toString))
- case None => None
- }
- ).groupMap(_._2)(e => LSP.Decoration_Options(e._1, Nil)).toList
-
- channel.write(output_json(text, Some(LSP.Decoration(decorations))))
- }
}
}
}
--- a/src/Tools/VSCode/src/state_panel.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Wed Aug 06 17:39:03 2025 +0200
@@ -80,7 +80,7 @@
def update(): Unit = {
server.editor.current_node_snapshot(()) match {
case Some(snapshot) =>
- (server.editor.current_command((), snapshot), print_state.get_location) match {
+ (server.editor.current_command(snapshot), print_state.get_location) match {
case (Some(command1), Some(command2)) if command1.id == command2.id =>
case _ => print_state.apply_query(Nil)
}
--- a/src/Tools/VSCode/src/vscode_model.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_model.scala Wed Aug 06 17:39:03 2025 +0200
@@ -144,7 +144,10 @@
def get_blob: Option[Document.Blobs.Item] =
if (is_theory) None
- else Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
+ else {
+ val changed = pending_edits.nonEmpty
+ Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, changed = changed))
+ }
/* data */
--- a/src/Tools/VSCode/src/vscode_resources.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Aug 06 17:39:03 2025 +0200
@@ -97,7 +97,7 @@
find_theory(file) getOrElse {
val node = file.getPath
val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
- if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+ if (loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
else Document.Node.Name(node, theory = theory)
}
@@ -336,6 +336,12 @@
def output_xml_text(body: XML.Tree): String = output_text(XML.content(body))
+ def output_text_xml(body: XML.Body): XML.Body =
+ body.map {
+ case XML.Elem(markup, body) => XML.Elem(markup, output_text_xml(body))
+ case XML.Text(content) => XML.Text(output_text(content))
+ }
+
def output_pretty(body: XML.Body, margin: Double): String =
output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric))
def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
--- a/src/Tools/jEdit/src/document_model.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Aug 06 17:39:03 2025 +0200
@@ -408,6 +408,9 @@
last_perspective: Document.Node.Perspective_Text.T,
pending_edits: List[Text.Edit]
) extends Document_Model {
+ override def toString: String = "file " + quote(node_name.node)
+
+
/* content */
def node_name: Document.Node.Name = content.node_name
@@ -436,7 +439,10 @@
def get_blob: Option[Document.Blobs.Item] =
if (is_theory) None
- else Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
+ else {
+ val changed = pending_edits.nonEmpty
+ Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, changed = changed))
+ }
def untyped_data: AnyRef = content.data
@@ -490,6 +496,9 @@
val node_name: Document.Node.Name,
val buffer: Buffer
) extends Document_Model {
+ override def toString: String = "buffer " + quote(node_name.node)
+
+
/* text */
def get_text(range: Text.Range): Option[String] =
@@ -590,8 +599,7 @@
blob = Some(x)
x
}
- val changed = !is_stable
- Some(Document.Blobs.Item(bytes, text, chunk, changed))
+ Some(Document.Blobs.Item(bytes, text, chunk, changed = !is_stable))
}
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Wed Aug 06 17:39:03 2025 +0200
@@ -78,23 +78,21 @@
override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
GUI_Thread.require { Document_Model.get_snapshot(name) getOrElse session.snapshot(name) }
- override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = {
- GUI_Thread.require {}
-
- val text_area = view.getTextArea
- val buffer = view.getBuffer
+ override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
+ GUI_Thread.require {
+ val text_area = view.getTextArea
+ val caret_offset = text_area.getCaretPosition
+ Document_View.get(text_area) match {
+ case Some(doc_view) if snapshot.loaded_theory_command(caret_offset).isEmpty =>
+ snapshot.current_command(doc_view.model.node_name, caret_offset)
+ case _ => None
+ }
+ }
- Document_View.get(text_area) match {
- case Some(doc_view) if doc_view.model.is_theory =>
- snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition)
- case _ =>
- Document_Model.get_model(buffer) match {
- case Some(model) if !model.is_theory =>
- snapshot.version.nodes.commands_loading(model.node_name).headOption
- case _ => None
- }
- }
- }
+
+ /* output messages */
+
+ override def output_state(): Boolean = JEdit_Options.output_state()
/* overlays */
--- a/src/Tools/jEdit/src/jedit_resources.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Aug 06 17:39:03 2025 +0200
@@ -34,7 +34,7 @@
val vfs = VFSManager.getVFSForPath(path)
val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
- if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+ if (loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
else Document.Node.Name(node, theory = theory)
}
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Aug 06 17:39:03 2025 +0200
@@ -35,26 +35,17 @@
override def detach_operation: Option[() => Unit] =
output.pretty_text_area.detach_operation
- private def handle_update(
- follow: Boolean = true,
- restriction: Option[Set[Command]] = None
- ): Unit = {
- GUI_Thread.require {}
-
- for {
- snapshot <- PIDE.editor.current_node_snapshot(view)
- if follow && !snapshot.is_outdated
- command <- PIDE.editor.current_command(view, snapshot)
- if restriction.isEmpty || restriction.get.contains(command)
- } {
- val results = snapshot.command_results(command)
- val new_output = Rendering.output_messages(results, JEdit_Options.output_state())
- if (current_output != new_output) {
- output.pretty_text_area.update(snapshot, results, new_output)
- current_output = new_output
+ private def handle_update(restriction: Option[Set[Command]] = None): Unit =
+ GUI_Thread.require {
+ val caret_offset = view.getTextArea.getCaretPosition
+ for (snapshot <- PIDE.editor.current_node_snapshot(view)) {
+ val output = PIDE.editor.output(snapshot, caret_offset, restriction = restriction)
+ if (output.defined && current_output != output.messages) {
+ dockable.output.pretty_text_area.update(snapshot, output.results, output.messages)
+ current_output = output.messages
+ }
}
}
- }
output.setup(dockable)
dockable.set_content(output.split_pane)
@@ -70,7 +61,7 @@
tooltip = "Indicate automatic update following cursor movement"
override def clicked(state: Boolean): Unit = {
do_update = state
- handle_update(follow = do_update)
+ if (do_update) handle_update()
}
}
@@ -96,15 +87,15 @@
output.handle_resize()
output_state_button.load()
auto_hovering_button.load()
- handle_update(do_update)
+ if (do_update) handle_update()
}
case changed: Session.Commands_Changed =>
val restriction = if (changed.assignment) None else Some(changed.commands)
- GUI_Thread.later { handle_update(follow = do_update, restriction = restriction) }
+ GUI_Thread.later { if (do_update) handle_update(restriction = restriction) }
case Session.Caret_Focus =>
- GUI_Thread.later { handle_update(follow = do_update) }
+ GUI_Thread.later { if (do_update) handle_update() }
}
override def init(): Unit = {
--- a/src/Tools/jEdit/src/theories_status.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/jEdit/src/theories_status.scala Wed Aug 06 17:39:03 2025 +0200
@@ -26,7 +26,7 @@
private var document_required = Set.empty[Document.Node.Name]
private def is_loaded_theory(name: Document.Node.Name): Boolean =
- PIDE.resources.session_base.loaded_theory(name)
+ PIDE.resources.loaded_theory(name)
private def overall_node_status(name: Document.Node.Name): Document_Status.Overall_Node_Status = {
if (is_loaded_theory(name)) Document_Status.Overall_Node_Status.ok
--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Aug 06 16:51:58 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Aug 06 17:39:03 2025 +0200
@@ -169,7 +169,7 @@
case None => snapshot.version.nodes.iterator
}).foldLeft(nodes_timing) {
case (timing1, (name, node)) =>
- if (PIDE.resources.session_base.loaded_theory(name)) timing1
+ if (PIDE.resources.loaded_theory(name)) timing1
else {
val node_timing =
Document_Status.Overall_Timing.make(