tuned signature;
authorwenzelm
Sat Mar 29 09:34:51 2014 +0100 (2014-03-29)
changeset 563149a513737a0b2
parent 56313 84d047625f70
child 56315 c20053f67093
tuned signature;
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Mar 29 09:24:39 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Mar 29 09:34:51 2014 +0100
     1.3 @@ -57,13 +57,13 @@
     1.4    def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
     1.5    def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
     1.6  
     1.7 -  def thy_load(span: List[Token]): Option[List[String]] =
     1.8 +  def load(span: List[Token]): Option[List[String]] =
     1.9      keywords.get(Command.name(span)) match {
    1.10        case Some((Keyword.THY_LOAD, exts)) => Some(exts)
    1.11        case _ => None
    1.12      }
    1.13  
    1.14 -  val thy_load_commands: List[(String, List[String])] =
    1.15 +  val load_commands: List[(String, List[String])] =
    1.16      (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
    1.17  
    1.18    def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Mar 29 09:24:39 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Mar 29 09:34:51 2014 +0100
     2.3 @@ -189,7 +189,7 @@
     2.4  
     2.5      final class Commands private(val commands: Linear_Set[Command])
     2.6      {
     2.7 -      lazy val thy_load_commands: List[Command] =
     2.8 +      lazy val load_commands: List[Command] =
     2.9          commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
    2.10  
    2.11        private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
    2.12 @@ -244,7 +244,7 @@
    2.13        perspective.overlays == other_perspective.overlays
    2.14  
    2.15      def commands: Linear_Set[Command] = _commands.commands
    2.16 -    def thy_load_commands: List[Command] = _commands.thy_load_commands
    2.17 +    def load_commands: List[Command] = _commands.load_commands
    2.18  
    2.19      def update_commands(new_commands: Linear_Set[Command]): Node =
    2.20        if (new_commands eq _commands.commands) this
    2.21 @@ -290,10 +290,10 @@
    2.22      def entries: Iterator[(Node.Name, Node)] =
    2.23        graph.entries.map({ case (name, (node, _)) => (name, node) })
    2.24  
    2.25 -    def thy_load_commands(file_name: Node.Name): List[Command] =
    2.26 +    def load_commands(file_name: Node.Name): List[Command] =
    2.27        (for {
    2.28          (_, node) <- entries
    2.29 -        cmd <- node.thy_load_commands.iterator
    2.30 +        cmd <- node.load_commands.iterator
    2.31          name <- cmd.blobs_names.iterator
    2.32          if name == file_name
    2.33        } yield cmd).toList
    2.34 @@ -421,7 +421,7 @@
    2.35  
    2.36      val node_name: Node.Name
    2.37      val node: Node
    2.38 -    val thy_load_commands: List[Command]
    2.39 +    val load_commands: List[Command]
    2.40      def is_loaded: Boolean
    2.41      def eq_content(other: Snapshot): Boolean
    2.42  
    2.43 @@ -694,11 +694,11 @@
    2.44          val node_name = name
    2.45          val node = version.nodes(name)
    2.46  
    2.47 -        val thy_load_commands: List[Command] =
    2.48 +        val load_commands: List[Command] =
    2.49            if (node_name.is_theory) Nil
    2.50 -          else version.nodes.thy_load_commands(node_name)
    2.51 +          else version.nodes.load_commands(node_name)
    2.52  
    2.53 -        val is_loaded: Boolean = node_name.is_theory || !thy_load_commands.isEmpty
    2.54 +        val is_loaded: Boolean = node_name.is_theory || !load_commands.isEmpty
    2.55  
    2.56          def eq_content(other: Snapshot): Boolean =
    2.57          {
    2.58 @@ -713,8 +713,8 @@
    2.59            !is_outdated && !other.is_outdated &&
    2.60            node.commands.size == other.node.commands.size &&
    2.61            (node.commands.iterator zip other.node.commands.iterator).forall(eq_commands) &&
    2.62 -          thy_load_commands.length == other.thy_load_commands.length &&
    2.63 -          (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
    2.64 +          load_commands.length == other.load_commands.length &&
    2.65 +          (load_commands zip other.load_commands).forall(eq_commands)
    2.66          }
    2.67  
    2.68  
    2.69 @@ -729,7 +729,7 @@
    2.70          {
    2.71            val former_range = revert(range)
    2.72            val (file_name, command_range_iterator) =
    2.73 -            thy_load_commands match {
    2.74 +            load_commands match {
    2.75                case command :: _ => (node_name.node, Iterator((command, 0)))
    2.76                case _ => ("", node.command_range(former_range))
    2.77              }
     3.1 --- a/src/Pure/PIDE/resources.scala	Sat Mar 29 09:24:39 2014 +0100
     3.2 +++ b/src/Pure/PIDE/resources.scala	Sat Mar 29 09:34:51 2014 +0100
     3.3 @@ -51,7 +51,7 @@
     3.4    /* theory files */
     3.5  
     3.6    def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
     3.7 -    syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
     3.8 +    syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
     3.9  
    3.10    def body_files(syntax: Outer_Syntax, text: String): List[String] =
    3.11    {
     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 09:24:39 2014 +0100
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 09:34:51 2014 +0100
     4.3 @@ -245,7 +245,7 @@
     4.4    }
     4.5  
     4.6    def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =
     4.7 -    syntax.thy_load(span) match {
     4.8 +    syntax.load(span) match {
     4.9        case Some(exts) =>
    4.10          find_file(span) match {
    4.11            case Some(file) =>
    4.12 @@ -448,7 +448,7 @@
    4.13        val reparse =
    4.14          (reparse0 /: nodes0.entries)({
    4.15            case (reparse, (name, node)) =>
    4.16 -            if (node.thy_load_commands.exists(_.blobs_changed(doc_blobs)))
    4.17 +            if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
    4.18                name :: reparse
    4.19              else reparse
    4.20            })
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Mar 29 09:24:39 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Mar 29 09:34:51 2014 +0100
     5.3 @@ -115,9 +115,9 @@
     5.4          }
     5.5          else Nil
     5.6  
     5.7 -      val thy_load_ranges =
     5.8 +      val load_ranges =
     5.9          for {
    5.10 -          cmd <- snapshot.node.thy_load_commands
    5.11 +          cmd <- snapshot.node.load_commands
    5.12            blob_name <- cmd.blobs_names
    5.13            blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
    5.14            if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
    5.15 @@ -125,11 +125,11 @@
    5.16            range = snapshot.convert(cmd.proper_range + start)
    5.17          } yield range
    5.18  
    5.19 -      val reparse = snapshot.node.thy_load_commands.exists(_.blobs_changed(doc_blobs))
    5.20 +      val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs))
    5.21  
    5.22        (reparse,
    5.23          Document.Node.Perspective(node_required,
    5.24 -          Text.Perspective(document_view_ranges ::: thy_load_ranges),
    5.25 +          Text.Perspective(document_view_ranges ::: load_ranges),
    5.26            PIDE.editor.node_overlays(node_name)))
    5.27      }
    5.28      else (false, empty_perspective)
     6.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Mar 29 09:24:39 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Mar 29 09:34:51 2014 +0100
     6.3 @@ -210,17 +210,17 @@
     6.4                if (model.buffer == text_area.getBuffer) {
     6.5                  val snapshot = model.snapshot()
     6.6  
     6.7 -                val thy_load_changed =
     6.8 -                  snapshot.thy_load_commands.exists(changed.commands.contains)
     6.9 +                val load_changed =
    6.10 +                  snapshot.load_commands.exists(changed.commands.contains)
    6.11  
    6.12 -                if (changed.assignment || thy_load_changed ||
    6.13 +                if (changed.assignment || load_changed ||
    6.14                      (changed.nodes.contains(model.node_name) &&
    6.15                       changed.commands.exists(snapshot.node.commands.contains)))
    6.16                    Swing_Thread.later { overview.delay_repaint.invoke() }
    6.17  
    6.18                  val visible_lines = text_area.getVisibleLines
    6.19                  if (visible_lines > 0) {
    6.20 -                  if (changed.assignment || thy_load_changed)
    6.21 +                  if (changed.assignment || load_changed)
    6.22                      text_area.invalidateScreenLineRange(0, visible_lines)
    6.23                    else {
    6.24                      val visible_range = JEdit_Lib.visible_range(text_area).get
     7.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Mar 29 09:24:39 2014 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Mar 29 09:34:51 2014 +0100
     7.3 @@ -85,7 +85,7 @@
     7.4        case _ =>
     7.5          PIDE.document_model(buffer) match {
     7.6            case Some(model) if !model.is_theory =>
     7.7 -            snapshot.version.nodes.thy_load_commands(model.node_name) match {
     7.8 +            snapshot.version.nodes.load_commands(model.node_name) match {
     7.9                case cmd :: _ => Some(cmd)
    7.10                case Nil => None
    7.11              }