# HG changeset patch
# User wenzelm
# Date 1754490853 -7200
# Node ID b99b7acfbc24d0ebd7db83ea974df81a3f882465
# Parent  cbf3703f92ea409c2ff138c08ce18fb51397b0aa# Parent  adaea1a92086bfadf3ad419d4ca2ed7516e4b4dc
merged

diff -r cbf3703f92ea -r b99b7acfbc24 NEWS
--- a/NEWS	Wed Aug 06 10:01:05 2025 +0100
+++ b/NEWS	Wed Aug 06 16:34:13 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:
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/Build/build.scala	Wed Aug 06 16:34:13 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]
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/Build/build_job.scala	Wed Aug 06 16:34:13 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()
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/Build/export.scala
--- a/src/Pure/Build/export.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/Build/export.scala	Wed Aug 06 16:34:13 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) + ")"
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/Build/resources.scala
--- a/src/Pure/Build/resources.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/Build/resources.scala	Wed Aug 06 16:34:13 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] = {
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/Build/sessions.scala
--- a/src/Pure/Build/sessions.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/Build/sessions.scala	Wed Aug 06 16:34:13 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))
                 }
 
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 06 16:34:13 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 *)
 
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Aug 06 16:34:13 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
 
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/command_span.ML
--- a/src/Pure/PIDE/command_span.ML	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/command_span.ML	Wed Aug 06 16:34:13 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;
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/command_span.scala	Wed Aug 06 16:34:13 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)
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Aug 06 16:34:13 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)))
                 }
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Wed Aug 06 16:34:13 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)
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/document_info.scala
--- a/src/Pure/PIDE/document_info.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/document_info.scala	Wed Aug 06 16:34:13 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)
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/document_status.scala	Wed Aug 06 16:34:13 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)
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/editor.scala	Wed Aug 06 16:34:13 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
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/headless.scala	Wed Aug 06 16:34:13 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
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Aug 06 16:34:13 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)];
 
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Aug 06 16:34:13 2025 +0200
@@ -464,6 +464,8 @@
       else None
   }
 
+  val COMMAND_RANGE = "command_range"
+
   val COMMAND = "command"
   val KEYWORD = "keyword"
   val KEYWORD1 = "keyword1"
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Aug 06 16:34:13 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))) }))
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Aug 06 16:34:13 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 */
 
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/session.scala	Wed Aug 06 16:34:13 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)
                     }
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/PIDE/text.scala	Wed Aug 06 16:34:13 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 */
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/ROOT.ML	Wed Aug 06 16:34:13 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.
 
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 06 16:34:13 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 =
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 06 16:34:13 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)))
             }
 
diff -r cbf3703f92ea -r b99b7acfbc24 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/Tools/dump.scala	Wed Aug 06 16:34:13 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 + ")")
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Wed Aug 06 16:34:13 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 = {
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Aug 06 16:34:13 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 =
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Wed Aug 06 16:34:13 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))))
-      }
     }
   }
 }
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/VSCode/src/state_panel.scala	Wed Aug 06 16:34:13 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)
         }
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Wed Aug 06 16:34:13 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 */
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Aug 06 16:34:13 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)
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 06 16:34:13 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))
       }
     }
 
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Aug 06 16:34:13 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 */
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Aug 06 16:34:13 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)
     }
 
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Aug 06 16:34:13 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 = {
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/jEdit/src/theories_status.scala
--- a/src/Tools/jEdit/src/theories_status.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala	Wed Aug 06 16:34:13 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
diff -r cbf3703f92ea -r b99b7acfbc24 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Aug 06 16:34:13 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(