src/Pure/PIDE/command_span.scala

--- a/src/Pure/PIDE/command_span.scala	Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala	Mon Nov 23 15:14:58 2020 +0100
@@ -18,14 +18,18 @@
         case Command_Span(name, _) => proper_string(name) getOrElse "<command>"
         case Ignored_Span => "<ignored>"
         case Malformed_Span => "<malformed>"
+        case Theory_Span => "<theory>"
       }
   }
   case class Command_Span(name: String, pos: Position.T) extends Kind
   case object Ignored_Span extends Kind
   case object Malformed_Span extends Kind
+  case object Theory_Span extends Kind
 
   sealed case class Span(kind: Kind, content: List[Token])
   {
+    def is_theory: Boolean = kind == Theory_Span
+
     def name: String =
       kind match { case Command_Span(name, _) => name case _ => "" }
 
@@ -67,8 +71,11 @@
 
   val empty: Span = Span(Ignored_Span, Nil)
 
-  def unparsed(source: String): Span =
-    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
+  def unparsed(source: String, theory: Boolean): Span =
+  {
+    val kind = if (theory) Theory_Span else Malformed_Span
+    Span(kind, List(Token(Token.Kind.UNPARSED, source)))
+  }
 
 
   /* XML data representation */