Isabelle2018 support

.travis.yml

@@ -13,7 +13,7 @@ matrix:
     - env: ISABELLE_VERSION=stable:2017 SCALA_VERSION=2.11.12 PROFILE=quick
       os: osx
       osx_image: xcode8.3
-    - env: ISABELLE_VERSION=stable:2018-RC2 SCALA_VERSION=2.11.12 PROFILE=quick
+    - env: ISABELLE_VERSION=stable:2018 SCALA_VERSION=2.11.12 PROFILE=quick
       os: osx
       osx_image: xcode8.3
     - env: ISABELLE_VERSION=stable:2016 SCALA_VERSION=2.11.12 PROFILE=generic
@@ -44,7 +44,7 @@ matrix:
         apt:
           packages:
             - lib32stdc++6
-    - env: ISABELLE_VERSION=stable:2018-RC2 SCALA_VERSION=2.12.6 PROFILE=slow
+    - env: ISABELLE_VERSION=stable:2018 SCALA_VERSION=2.12.6 PROFILE=slow
       os: linux
       jdk: oraclejdk8
       addons:

appveyor.yml

@@ -5,7 +5,7 @@ platform:
   - x64
 environment:
   matrix:
-    - ISABELLE_VERSION: 2018-RC2
+    - ISABELLE_VERSION: 2018
 build_script:
   - sbt compile
 test_script:

build.sbt

@@ -224,11 +224,11 @@ def pide(version: String) = Project(s"pide$version", file(s"modules/pide/$versio
   )
 
 lazy val pide2017 = pide("2017")
-lazy val pide2018_RC2 = pide("2018-RC2")
+lazy val pide2018 = pide("2018")
 
 lazy val pides = Seq(
   pide2017,
-  pide2018_RC2
+  pide2018
 )
 
 inThisBuild(pides.map { p =>

modules/pide/2018-RC2/src/main/scala/Isar/line_structure.scala → modules/pide/2018/src/main/scala/Isar/line_structure.scala

@@ -23,7 +23,7 @@ sealed case class Line_Structure(
 {
   def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure =
   {
-    val improper1 = tokens.forall(_.is_improper)
+    val improper1 = tokens.forall(tok => !tok.is_proper)
     val blank1 = tokens.forall(_.is_space)
     val command1 = tokens.exists(_.is_begin_or_command)
 

modules/pide/2018-RC2/src/main/scala/Isar/outer_syntax.scala → modules/pide/2018/src/main/scala/Isar/outer_syntax.scala

@@ -161,12 +161,12 @@ final class Outer_Syntax private(
   {
     val result = new mutable.ListBuffer[Command_Span.Span]
     val content = new mutable.ListBuffer[Token]
-    val improper = new mutable.ListBuffer[Token]
+    val ignored = new mutable.ListBuffer[Token]
 
     def ship(span: List[Token])
     {
       val kind =
-        if (span.forall(_.is_improper)) Command_Span.Ignored_Span
+        if (span.forall(_.is_ignored)) Command_Span.Ignored_Span
         else if (span.exists(_.is_error)) Command_Span.Malformed_Span
         else
           span.find(_.is_command) match {
@@ -186,16 +186,16 @@ final class Outer_Syntax private(
     def flush()
     {
       if (content.nonEmpty) { ship(content.toList); content.clear }
-      if (improper.nonEmpty) { ship(improper.toList); improper.clear }
+      if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear }
     }
 
     for (tok <- toks) {
-      if (tok.is_improper) improper += tok
+      if (tok.is_ignored) ignored += tok
       else if (keywords.is_before_command(tok) ||
         tok.is_command &&
           (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
       { flush(); content += tok }
-      else { content ++= improper; improper.clear; content += tok }
+      else { content ++= ignored; ignored.clear; content += tok }
     }
     flush()
 

modules/pide/2018-RC2/src/main/scala/Isar/token.scala → modules/pide/2018/src/main/scala/Isar/token.scala

@@ -296,7 +296,7 @@ sealed case class Token(kind: Token.Kind.Value, source: String)
   def is_informal_comment: Boolean = kind == Token.Kind.INFORMAL_COMMENT
   def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT
   def is_comment: Boolean = is_informal_comment || is_formal_comment
-  def is_improper: Boolean = is_space || is_comment
+  def is_ignored: Boolean = is_space || is_informal_comment
   def is_proper: Boolean = !is_space && !is_comment
   def is_error: Boolean = kind == Token.Kind.ERROR
   def is_unparsed: Boolean = kind == Token.Kind.UNPARSED

modules/pide/2018-RC2/src/main/scala/PIDE/command.scala → modules/pide/2018/src/main/scala/PIDE/command.scala

@@ -319,7 +319,7 @@ object Command
               case elem @ XML.Elem(markup, Nil) =>
                 state.
                   add_status(markup).
-                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
+                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
               case _ =>
                 Output.warning("Ignored status message: " + msg)
                 state
@@ -355,7 +355,7 @@ object Command
 
                 case XML.Elem(Markup(name, atts), args)
                 if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
-                  val range = command.proper_range
+                  val range = command.core_range
                   val props = Position.purge(atts)
                   val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
                   state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem))
@@ -603,9 +603,9 @@ final class Command private(
   def length: Int = source.length
   def range: Text.Range = chunk.range
 
-  val proper_range: Text.Range =
+  val core_range: Text.Range =
     Text.Range(0,
-      (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
+      (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
 
   def source(range: Text.Range): String = range.substring(source)
 

modules/pide/2018-RC2/src/main/scala/PIDE/document.scala → modules/pide/2018/src/main/scala/PIDE/document.scala

@@ -1024,7 +1024,7 @@ object Document
             blob_name <- cmd.blobs_names.iterator
             if pred(blob_name)
             start <- node.command_start(cmd)
-          } yield convert(cmd.proper_range + start)).toList
+          } yield convert(cmd.core_range + start)).toList
 
         def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
           if (other_node_name.is_theory) {

modules/pide/2018-RC2/src/main/scala/System/distribution.scala → modules/pide/2018/src/main/scala/System/distribution.scala

@@ -9,7 +9,7 @@ package isabelle
 
 object Distribution
 {
-  val version = "Isabelle2018-RC2: July 2018"
+  val version = "Isabelle2018: August 2018"
   val is_identified = true
   val is_official = false
 }

modules/pide/2018-RC2/src/main/scala/Thy/present.scala → modules/pide/2018/src/main/scala/Thy/present.scala

@@ -277,8 +277,8 @@ object Present
         "Failed to build document in " + File.path(dir.absolute_file))
     }
 
-    bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
-      root_bash(document_format) + " " + File.bash_path(document_target)).check
+    bash("if [ -f " + root_bash(document_format) + " ]; then cp -f " +
+      root_bash(document_format) + " " + File.bash_path(document_target) + "; fi").check
   }
 
 

modules/pide/2018-RC2/src/main/scala/Thy/sessions.scala → modules/pide/2018/src/main/scala/Thy/sessions.scala

@@ -587,36 +587,6 @@ object Sessions
         exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
         session_groups = Library.merge(session_groups, other.session_groups),
         sessions = Library.merge(sessions, other.sessions))
-
-    def selected(graph: Graph[String, Info]): List[String] =
-    {
-      val select_group = session_groups.toSet
-      val select_session = sessions.toSet ++ graph.all_succs(base_sessions)
-
-      val selected0 =
-        if (all_sessions) graph.keys
-        else {
-          (for {
-            (name, (info, _)) <- graph.iterator
-            if info.dir_selected || select_session(name) ||
-              graph.get_node(name).groups.exists(select_group)
-          } yield name).toList
-        }
-
-      if (requirements) (graph.all_preds(selected0).toSet -- selected0).toList
-      else selected0
-    }
-
-    def excluded(graph: Graph[String, Info]): List[String] =
-    {
-      val exclude_group = exclude_session_groups.toSet
-      val exclude_group_sessions =
-        (for {
-          (name, (info, _)) <- graph.iterator
-          if graph.get_node(name).groups.exists(exclude_group)
-        } yield name).toList
-      graph.all_succs(exclude_group_sessions ::: exclude_sessions)
-    }
   }
 
   def make(infos: List[Info]): Structure =
@@ -690,15 +660,48 @@ object Sessions
         error("Undefined session(s): " + commas_quote(bad_sessions))
     }
 
+    def check_sessions(sel: Selection): Unit =
+      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
+
+    private def selected(graph: Graph[String, Info], sel: Selection): List[String] =
+    {
+      check_sessions(sel)
+
+      val select_group = sel.session_groups.toSet
+      val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions)
+
+      val selected0 =
+        if (sel.all_sessions) graph.keys
+        else {
+          (for {
+            (name, (info, _)) <- graph.iterator
+            if info.dir_selected || select_session(name) ||
+              graph.get_node(name).groups.exists(select_group)
+          } yield name).toList
+        }
+
+      if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
+      else selected0
+    }
+
     def selection(sel: Selection): Structure =
     {
-      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
+      check_sessions(sel)
 
-      val excluded = sel.excluded(build_graph).toSet
+      val excluded =
+      {
+        val exclude_group = sel.exclude_session_groups.toSet
+        val exclude_group_sessions =
+          (for {
+            (name, (info, _)) <- imports_graph.iterator
+            if imports_graph.get_node(name).groups.exists(exclude_group)
+          } yield name).toList
+        imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
+      }
 
       def restrict(graph: Graph[String, Info]): Graph[String, Info] =
       {
-        val sessions = graph.all_preds(sel.selected(graph)).filterNot(excluded)
+        val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
         graph.restrict(graph.all_preds(sessions).toSet)
       }
 
@@ -714,12 +717,12 @@ object Sessions
         progress = progress, inlined_files = inlined_files, verbose = verbose)
     }
 
-    def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
+    def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
     def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
     def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse
     def build_topological_order: List[String] = build_graph.topological_order
 
-    def imports_selection(sel: Selection): List[String] = sel.selected(imports_graph)
+    def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
     def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
     def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds(ss).reverse
     def imports_topological_order: List[String] = imports_graph.topological_order

modules/pide/2018-RC2/src/main/scala/Thy/thy_resources.scala → modules/pide/2018/src/main/scala/Thy/thy_resources.scala

@@ -71,6 +71,9 @@ object Thy_Resources
     }
   }
 
+  val default_use_theories_check_delay: Double = 0.5
+
+
   class Session private[Thy_Resources](
     session_name: String,
     session_options: Options,
@@ -96,6 +99,8 @@ object Thy_Resources
       theories: List[String],
       qualifier: String = Sessions.DRAFT,
       master_dir: String = "",
+      check_delay: Time = Time.seconds(default_use_theories_check_delay),
+      check_limit: Int = 0,
       id: UUID = UUID(),
       progress: Progress = No_Progress): Theories_Result =
     {
@@ -105,23 +110,34 @@ object Thy_Resources
 
       val result = Future.promise[Theories_Result]
 
-      def check_state
+      def check_state(beyond_limit: Boolean = false)
       {
         val state = session.current_state()
         state.stable_tip_version match {
-          case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) =>
-            val nodes =
-              for (name <- dep_theories)
-              yield (name -> Protocol.node_status(state, version, name))
-            try { result.fulfill(new Theories_Result(state, version, nodes)) }
-            catch { case _: IllegalStateException => }
-          case _ =>
+          case Some(version) =>
+            if (beyond_limit || dep_theories.forall(state.node_consolidated(version, _))) {
+              val nodes =
+                for (name <- dep_theories)
+                yield (name -> Protocol.node_status(state, version, name))
+              try { result.fulfill(new Theories_Result(state, version, nodes)) }
+              catch { case _: IllegalStateException => }
+            }
+          case None =>
         }
       }
 
       val check_progress =
-        Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5)))
-          { if (progress.stopped) result.cancel else check_state }
+      {
+        var check_count = 0
+        Event_Timer.request(Time.now(), repeat = Some(check_delay))
+          {
+            if (progress.stopped) result.cancel
+            else {
+              check_count += 1
+              check_state(check_limit > 0 && check_count > check_limit)
+            }
+          }
+      }
 
       val theories_progress = Synchronized(Set.empty[Document.Node.Name])
 
@@ -147,7 +163,7 @@ object Thy_Resources
                 initialized.map(_.theory).sorted.foreach(progress.theory("", _))
               }
 
-              check_state
+              check_state()
             }
         }
 

modules/pide/2018-RC2/src/main/scala/Tools/build.scala → modules/pide/2018/src/main/scala/Tools/build.scala

@@ -64,15 +64,16 @@ object Build
       }
     }
 
-    def make_session_timing(sessions: Sessions.Structure, timing: Map[String, Double])
+    def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
       : Map[String, Double] =
     {
-      val maximals = sessions.build_graph.maximals.toSet
+      val maximals = sessions_structure.build_graph.maximals.toSet
       def desc_timing(name: String): Double =
       {
         if (maximals.contains(name)) timing(name)
         else {
-          val g = sessions.build_graph.restrict(sessions.build_descendants(List(name)).toSet)
+          val descendants = sessions_structure.build_descendants(List(name)).toSet
+          val g = sessions_structure.build_graph.restrict(descendants)
           (0.0 :: g.maximals.flatMap(desc => {
             val ps = g.all_preds(List(desc))
             if (ps.exists(p => timing.get(p).isEmpty)) None
@@ -83,16 +84,18 @@ object Build
       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
     }
 
-    def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
+    def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
+      : Queue =
     {
-      val graph = sessions.build_graph
+      val graph = sessions_structure.build_graph
       val names = graph.keys
 
       val timings = names.map(name => (name, load_timings(progress, store, name)))
       val command_timings =
         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
       val session_timing =
-        make_session_timing(sessions, timings.map({ case (name, (_, t)) => (name, t) }).toMap)
+        make_session_timing(sessions_structure,
+          timings.map({ case (name, (_, t)) => (name, t) }).toMap)
 
       object Ordering extends scala.math.Ordering[String]
       {
@@ -107,7 +110,7 @@ object Build
         def compare(name1: String, name2: String): Int =
           compare_timing(name2, name1) match {
             case 0 =>
-              sessions(name2).timeout compare sessions(name1).timeout match {
+              sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
                 case 0 => name1 compare name2
                 case ord => ord
               }
@@ -489,7 +492,7 @@ object Build
     store.prepare_output_dir()
 
     if (clean_build) {
-      for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
+      for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) {
         val (relevant, ok) = store.clean_output(name)
         if (relevant) {
           if (ok) progress.echo("Cleaned " + name)