# HG changeset patch
# User wenzelm
# Date 1384705375 -3600
# Node ID c9bb763033482a208d0e474e49b4de0c1e8d9815
# Parent  6c360a6ade0e35dc46a293b8a67a62d3e4a58fe4
explicit indication of thy_load commands;

diff -r 6c360a6ade0e -r c9bb76303348 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Sun Nov 17 16:02:06 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Sun Nov 17 17:22:55 2013 +0100
@@ -56,6 +56,12 @@
   def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
   def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
 
+  def thy_load(span: List[Token]): Option[List[String]] =
+    keywords.get(Command.name(span)) match {
+      case Some((Keyword.THY_LOAD, files)) => Some(files)
+      case _ => None
+    }
+
   def thy_load_commands: List[(String, List[String])] =
     (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
 
diff -r 6c360a6ade0e -r c9bb76303348 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Nov 17 16:02:06 2013 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Nov 17 17:22:55 2013 +0100
@@ -141,12 +141,14 @@
 
   /* make commands */
 
-  type Span = List[Token]
+  def name(span: List[Token]): String =
+    span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
 
   def apply(
     id: Document_ID.Command,
     node_name: Document.Node.Name,
-    span: Span,
+    span: List[Token],
+    thy_load: Option[List[String]],
     results: Results = Results.empty,
     markup: Markup_Tree = Markup_Tree.empty): Command =
   {
@@ -165,14 +167,15 @@
       i += n
     }
 
-    new Command(id, node_name, span1.toList, source, results, markup)
+    new Command(id, node_name, span1.toList, source, thy_load, results, markup)
   }
 
-  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil)
+  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, None)
 
   def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
       : Command =
-    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
+    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), None,
+      results, markup)
 
   def unparsed(source: String): Command =
     unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
@@ -212,6 +215,7 @@
     val node_name: Document.Node.Name,
     val span: List[Token],
     val source: String,
+    val thy_load: Option[List[String]],
     val init_results: Command.Results,
     val init_markup: Markup_Tree)
 {
@@ -225,8 +229,7 @@
   val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error))
   def is_command: Boolean = !is_ignored && !is_malformed
 
-  def name: String =
-    span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
+  def name: String = Command.name(span)
 
   override def toString =
     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
diff -r 6c360a6ade0e -r c9bb76303348 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Nov 17 16:02:06 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Nov 17 17:22:55 2013 +0100
@@ -148,6 +148,9 @@
 
     final class Commands private(val commands: Linear_Set[Command])
     {
+      lazy val thy_load_commands: List[Command] =
+        commands.iterator.filter(_.thy_load.isDefined).toList
+
       private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
       {
         val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
@@ -197,6 +200,7 @@
       perspective.overlays == other_perspective.overlays
 
     def commands: Linear_Set[Command] = _commands.commands
+    def thy_load_commands: List[Command] = _commands.thy_load_commands
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
diff -r 6c360a6ade0e -r c9bb76303348 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Nov 17 16:02:06 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Nov 17 17:22:55 2013 +0100
@@ -68,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(Document_ID.none, node_name, span)))
+      spans.foreach(span => add(Command(Document_ID.none, node_name, span, syntax.thy_load(span))))
       result()
     }
   }
@@ -255,7 +255,8 @@
         commands
       case cmd :: _ =>
         val hook = commands.prev(cmd)
-        val inserted = spans2.map(span => Command(Document_ID.make(), name, span))
+        val inserted =
+          spans2.map(span => Command(Document_ID.make(), name, span, syntax.thy_load(span)))
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }