# HG changeset patch
# User wenzelm
# Date 1396082091 -3600
# Node ID 9a513737a0b2b4a726a20db500ab1136f4c2a743
# Parent  84d047625f70d29550056a6c3077bb58f92ccc72
tuned signature;

diff -r 84d047625f70 -r 9a513737a0b2 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Sat Mar 29 09:24:39 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Sat Mar 29 09:34:51 2014 +0100
@@ -57,13 +57,13 @@
   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]] =
+  def load(span: List[Token]): Option[List[String]] =
     keywords.get(Command.name(span)) match {
       case Some((Keyword.THY_LOAD, exts)) => Some(exts)
       case _ => None
     }
 
-  val thy_load_commands: List[(String, List[String])] =
+  val load_commands: List[(String, List[String])] =
     (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
 
   def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
diff -r 84d047625f70 -r 9a513737a0b2 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Mar 29 09:24:39 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Mar 29 09:34:51 2014 +0100
@@ -189,7 +189,7 @@
 
     final class Commands private(val commands: Linear_Set[Command])
     {
-      lazy val thy_load_commands: List[Command] =
+      lazy val load_commands: List[Command] =
         commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
 
       private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
@@ -244,7 +244,7 @@
       perspective.overlays == other_perspective.overlays
 
     def commands: Linear_Set[Command] = _commands.commands
-    def thy_load_commands: List[Command] = _commands.thy_load_commands
+    def load_commands: List[Command] = _commands.load_commands
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
@@ -290,10 +290,10 @@
     def entries: Iterator[(Node.Name, Node)] =
       graph.entries.map({ case (name, (node, _)) => (name, node) })
 
-    def thy_load_commands(file_name: Node.Name): List[Command] =
+    def load_commands(file_name: Node.Name): List[Command] =
       (for {
         (_, node) <- entries
-        cmd <- node.thy_load_commands.iterator
+        cmd <- node.load_commands.iterator
         name <- cmd.blobs_names.iterator
         if name == file_name
       } yield cmd).toList
@@ -421,7 +421,7 @@
 
     val node_name: Node.Name
     val node: Node
-    val thy_load_commands: List[Command]
+    val load_commands: List[Command]
     def is_loaded: Boolean
     def eq_content(other: Snapshot): Boolean
 
@@ -694,11 +694,11 @@
         val node_name = name
         val node = version.nodes(name)
 
-        val thy_load_commands: List[Command] =
+        val load_commands: List[Command] =
           if (node_name.is_theory) Nil
-          else version.nodes.thy_load_commands(node_name)
+          else version.nodes.load_commands(node_name)
 
-        val is_loaded: Boolean = node_name.is_theory || !thy_load_commands.isEmpty
+        val is_loaded: Boolean = node_name.is_theory || !load_commands.isEmpty
 
         def eq_content(other: Snapshot): Boolean =
         {
@@ -713,8 +713,8 @@
           !is_outdated && !other.is_outdated &&
           node.commands.size == other.node.commands.size &&
           (node.commands.iterator zip other.node.commands.iterator).forall(eq_commands) &&
-          thy_load_commands.length == other.thy_load_commands.length &&
-          (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
+          load_commands.length == other.load_commands.length &&
+          (load_commands zip other.load_commands).forall(eq_commands)
         }
 
 
@@ -729,7 +729,7 @@
         {
           val former_range = revert(range)
           val (file_name, command_range_iterator) =
-            thy_load_commands match {
+            load_commands match {
               case command :: _ => (node_name.node, Iterator((command, 0)))
               case _ => ("", node.command_range(former_range))
             }
diff -r 84d047625f70 -r 9a513737a0b2 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Mar 29 09:24:39 2014 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Mar 29 09:34:51 2014 +0100
@@ -51,7 +51,7 @@
   /* theory files */
 
   def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
-    syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+    syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
 
   def body_files(syntax: Outer_Syntax, text: String): List[String] =
   {
diff -r 84d047625f70 -r 9a513737a0b2 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 09:24:39 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 09:34:51 2014 +0100
@@ -245,7 +245,7 @@
   }
 
   def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =
-    syntax.thy_load(span) match {
+    syntax.load(span) match {
       case Some(exts) =>
         find_file(span) match {
           case Some(file) =>
@@ -448,7 +448,7 @@
       val reparse =
         (reparse0 /: nodes0.entries)({
           case (reparse, (name, node)) =>
-            if (node.thy_load_commands.exists(_.blobs_changed(doc_blobs)))
+            if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
               name :: reparse
             else reparse
           })
diff -r 84d047625f70 -r 9a513737a0b2 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Mar 29 09:24:39 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Mar 29 09:34:51 2014 +0100
@@ -115,9 +115,9 @@
         }
         else Nil
 
-      val thy_load_ranges =
+      val load_ranges =
         for {
-          cmd <- snapshot.node.thy_load_commands
+          cmd <- snapshot.node.load_commands
           blob_name <- cmd.blobs_names
           blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
           if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
@@ -125,11 +125,11 @@
           range = snapshot.convert(cmd.proper_range + start)
         } yield range
 
-      val reparse = snapshot.node.thy_load_commands.exists(_.blobs_changed(doc_blobs))
+      val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs))
 
       (reparse,
         Document.Node.Perspective(node_required,
-          Text.Perspective(document_view_ranges ::: thy_load_ranges),
+          Text.Perspective(document_view_ranges ::: load_ranges),
           PIDE.editor.node_overlays(node_name)))
     }
     else (false, empty_perspective)
diff -r 84d047625f70 -r 9a513737a0b2 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sat Mar 29 09:24:39 2014 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sat Mar 29 09:34:51 2014 +0100
@@ -210,17 +210,17 @@
               if (model.buffer == text_area.getBuffer) {
                 val snapshot = model.snapshot()
 
-                val thy_load_changed =
-                  snapshot.thy_load_commands.exists(changed.commands.contains)
+                val load_changed =
+                  snapshot.load_commands.exists(changed.commands.contains)
 
-                if (changed.assignment || thy_load_changed ||
+                if (changed.assignment || load_changed ||
                     (changed.nodes.contains(model.node_name) &&
                      changed.commands.exists(snapshot.node.commands.contains)))
                   Swing_Thread.later { overview.delay_repaint.invoke() }
 
                 val visible_lines = text_area.getVisibleLines
                 if (visible_lines > 0) {
-                  if (changed.assignment || thy_load_changed)
+                  if (changed.assignment || load_changed)
                     text_area.invalidateScreenLineRange(0, visible_lines)
                   else {
                     val visible_range = JEdit_Lib.visible_range(text_area).get
diff -r 84d047625f70 -r 9a513737a0b2 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Mar 29 09:24:39 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Mar 29 09:34:51 2014 +0100
@@ -85,7 +85,7 @@
       case _ =>
         PIDE.document_model(buffer) match {
           case Some(model) if !model.is_theory =>
-            snapshot.version.nodes.thy_load_commands(model.node_name) match {
+            snapshot.version.nodes.load_commands(model.node_name) match {
               case cmd :: _ => Some(cmd)
               case Nil => None
             }