# HG changeset patch
# User wenzelm
# Date 1533996175 -7200
# Node ID 682ff0e84387bbba681be62a0abfee4fb0cfb393
# Parent  0c62e3b4f4c03898141091181c7130a7e458db8e# Parent  ec0b2833cfc40e127ab34ca4f1fdb33fe80056c6
merged;

diff -r ec0b2833cfc4 -r 682ff0e84387 .hgtags
--- a/.hgtags	Mon Aug 06 11:06:43 2018 +0200
+++ b/.hgtags	Sat Aug 11 16:02:55 2018 +0200
@@ -38,3 +38,4 @@
 cf01d04e94d71e6cda86a7740377ad903f86706b Isabelle2018-RC1
 14167c321d222b3628414ed97fe65205f7b8bde0 Isabelle2018-RC2
 71aa5a9128c21cc7faf95f2969077ddd7b5c1118 Isabelle2018-RC3
+34b8ff7cb10962428de2cbd61a3e0fc705455dac Isabelle2018-RC4
diff -r ec0b2833cfc4 -r 682ff0e84387 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Mon Aug 06 11:06:43 2018 +0200
+++ b/Admin/Release/CHECKLIST	Sat Aug 11 16:02:55 2018 +0200
@@ -86,7 +86,7 @@
 
 - Docker image:
 
-  isabelle build_docker -E -t makarius/isabelle:Isabelle2017 Isabelle2017_app.tar.gz
+  isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2018 Isabelle2018_app.tar.gz
 
   https://hub.docker.com/r/makarius/isabelle
   https://docs.docker.com/docker-cloud/builds/push-images
diff -r ec0b2833cfc4 -r 682ff0e84387 Admin/components/main
--- a/Admin/components/main	Mon Aug 06 11:06:43 2018 +0200
+++ b/Admin/components/main	Sat Aug 11 16:02:55 2018 +0200
@@ -19,6 +19,5 @@
 spass-3.8ds-1
 sqlite-jdbc-3.23.1
 vampire-4.2.2
-verit-2016post
 xz-java-1.8
 z3-4.4.0pre-2
diff -r ec0b2833cfc4 -r 682ff0e84387 NEWS
--- a/NEWS	Mon Aug 06 11:06:43 2018 +0200
+++ b/NEWS	Sat Aug 11 16:02:55 2018 +0200
@@ -478,6 +478,11 @@
   - option -S: only observe changes of sources, not heap images
   - option -f: forces a fresh build
 
+* Command-line tool "isabelle build" options -c -x -B refer to
+descendants wrt. the session parent or import graph. Subtle
+INCOMPATIBILITY: options -c -x used to refer to the session parent graph
+only.
+
 * Command-line tool "isabelle build" takes "condition" options with the
 corresponding environment values into account, when determining the
 up-to-date status of a session.
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sat Aug 11 16:02:55 2018 +0200
@@ -365,9 +365,9 @@
 text \<open>
   In distant past, displays with $1024 \times 768$ or $1280 \times 1024$
   pixels were considered ``high resolution'' and bitmap fonts with 12 or 14
-  pixels as adequate for text rendering. In 2017, we routinely see much higher
-  resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or ``Ultra HD'' /
-  ``4K'' at $3840 \times 2160$.
+  pixels as adequate for text rendering. After 2016, we have routinely seen
+  much higher resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or
+  ``Ultra HD'' / ``4K'' at $3840 \times 2160$.
 
   GUI frameworks are usually lagging behind, with hard-wired icon sizes and
   tiny fonts. Java and jEdit do provide reasonable support for very high
@@ -1381,14 +1381,20 @@
 
   Completion via abbreviations like \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>-->\<close> depends on the semantic
   language context (\secref{sec:completion-context}). In contrast, backslash
-  sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require
-  additional interaction to confirm (via popup).
+  sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require additional
+  interaction to confirm (via popup). This is important in ambiguous
+  situations, e.g.\ for Isabelle document source, which may contain formal
+  symbols or informal {\LaTeX} macros. Backslash sequences also help when
+  input is broken, and thus escapes its normal semantic context: e.g.\
+  antiquotations or string literals in ML, which do not allow arbitrary
+  backslash sequences.
 
-  The latter is important in ambiguous situations, e.g.\ for Isabelle document
-  source, which may contain formal symbols or informal {\LaTeX} macros.
-  Backslash sequences also help when input is broken, and thus escapes its
-  normal semantic context: e.g.\ antiquotations or string literals in ML,
-  which do not allow arbitrary backslash sequences.
+  Special symbols like \<^verbatim>\<open>\<comment>\<close> or control symbols like \<^verbatim>\<open>\<^cancel>\<close>,
+  \<^verbatim>\<open>\<^latex>\<close>, \<^verbatim>\<open>\<^binding>\<close> can have an argument: completing on a name
+  prefix offers a template with an empty cartouche. Thus completion of \<^verbatim>\<open>\co\<close>
+  or \<^verbatim>\<open>\ca\<close> allows to compose formal document comments quickly.\<^footnote>\<open>It is
+  customary to put a space between \<^verbatim>\<open>\<comment>\<close> and its argument, while
+  control symbols do \<^emph>\<open>not\<close> allow extra space here.\<close>
 \<close>
 
 
@@ -1889,23 +1895,30 @@
   \label{fig:cite-completion}
   \end{figure}
 
-  Isabelle/jEdit also provides some support for editing \<^verbatim>\<open>.bib\<close> files
+  Isabelle/jEdit also provides IDE support for editing \<^verbatim>\<open>.bib\<close> files
   themselves. There is syntax highlighting based on entry types (according to
   standard Bib{\TeX} styles), a context-menu to compose entries
   systematically, and a SideKick tree view of the overall content; see
-  \figref{fig:bibtex-mode}.
+  \figref{fig:bibtex-mode}. Semantic checking with errors and warnings is
+  performed by the original \<^verbatim>\<open>bibtex\<close> tool using style \<^verbatim>\<open>plain\<close>: different
+  Bib{\TeX} styles may produce slightly different results.
 
   \begin{figure}[!htb]
   \begin{center}
   \includegraphics[scale=0.333]{bibtex-mode}
   \end{center}
-  \caption{Bib{\TeX} mode with context menu and SideKick tree view}
+  \caption{Bib{\TeX} mode with context menu, SideKick tree view, and
+    semantic output from the \<^verbatim>\<open>bibtex\<close> tool}
   \label{fig:bibtex-mode}
   \end{figure}
+
+  Regular document preview (\secref{sec:document-preview}) of \<^verbatim>\<open>.bib\<close> files
+  approximates the usual {\LaTeX} bibliography output in HTML (using style
+  \<^verbatim>\<open>unsort\<close>).
 \<close>
 
 
-section \<open>Document preview\<close>
+section \<open>Document preview \label{sec:document-preview}\<close>
 
 text \<open>
   The action @{action_def isabelle.preview} opens an HTML preview of the
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Doc/JEdit/document/bibtex-mode.png
Binary file src/Doc/JEdit/document/bibtex-mode.png has changed
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Doc/System/Sessions.thy	Sat Aug 11 16:02:55 2018 +0200
@@ -333,14 +333,14 @@
   completed by including all ancestors.
 
   \<^medskip>
-  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions. All descendants
-  are included.
+  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions to be included (all
+  descendants wrt.\ the session parent or import graph).
 
   \<^medskip>
-  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All
-  descendents of excluded sessions are removed from the selection as specified
-  above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
-  specified by session group membership.
+  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded (all
+  descendants wrt.\ the session parent or import graph). Option \<^verbatim>\<open>-X\<close> is
+  analogous to this, but excluded sessions are specified by session group
+  membership.
 
   \<^medskip>
   Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its
@@ -373,8 +373,8 @@
   of sessions, as required for other sessions to continue later on.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-c\<close> cleans all descendants of the selected sessions before
-  performing the specified build operation.
+  Option \<^verbatim>\<open>-c\<close> cleans the selected sessions (all descendants wrt.\ the session
+  parent or import graph) before performing the specified build operation.
 
   \<^medskip>
   Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/Isar/line_structure.scala
--- a/src/Pure/Isar/line_structure.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/Isar/line_structure.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -23,7 +23,7 @@
 {
   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)
 
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Aug 11 16:02:55 2018 +0200
@@ -233,7 +233,7 @@
 fun ship span =
   let
     val kind =
-      if forall Token.is_improper span then Command_Span.Ignored_Span
+      if forall Token.is_ignored span then Command_Span.Ignored_Span
       else if exists Token.is_error span then Command_Span.Malformed_Span
       else
         (case find_first Token.is_command span of
@@ -241,18 +241,18 @@
         | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd));
   in cons (Command_Span.Span (kind, span)) end;
 
-fun flush (result, content, improper) =
+fun flush (result, content, ignored) =
   result
   |> not (null content) ? ship (rev content)
-  |> not (null improper) ? ship (rev improper);
+  |> not (null ignored) ? ship (rev ignored);
 
-fun parse tok (result, content, improper) =
-  if Token.is_improper tok then (result, content, tok :: improper)
+fun parse tok (result, content, ignored) =
+  if Token.is_ignored tok then (result, content, tok :: ignored)
   else if Token.is_command_modifier tok orelse
     Token.is_command tok andalso
       (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
-  then (flush (result, content, improper), [tok], [])
-  else (result, tok :: (improper @ content), []);
+  then (flush (result, content, ignored), [tok], [])
+  else (result, tok :: (ignored @ content), []);
 
 in
 
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -161,12 +161,12 @@
   {
     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 @@
     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()
 
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/Isar/token.ML	Sat Aug 11 16:02:55 2018 +0200
@@ -43,10 +43,10 @@
   val is_command_modifier: T -> bool
   val ident_with: (string -> bool) -> T -> bool
   val is_proper: T -> bool
-  val is_improper: T -> bool
   val is_comment: T -> bool
   val is_informal_comment: T -> bool
   val is_formal_comment: T -> bool
+  val is_ignored: T -> bool
   val is_begin_ignore: T -> bool
   val is_end_ignore: T -> bool
   val is_error: T -> bool
@@ -227,12 +227,14 @@
 fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   | ident_with _ _ = false;
 
+fun is_ignored (Token (_, (Space, _), _)) = true
+  | is_ignored (Token (_, (Comment NONE, _), _)) = true
+  | is_ignored _ = false;
+
 fun is_proper (Token (_, (Space, _), _)) = false
   | is_proper (Token (_, (Comment _, _), _)) = false
   | is_proper _ = true;
 
-val is_improper = not o is_proper;
-
 fun is_comment (Token (_, (Comment _, _), _)) = true
   | is_comment _ = false;
 
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/Isar/token.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -296,7 +296,7 @@
   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
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Aug 11 16:02:55 2018 +0200
@@ -136,11 +136,11 @@
   let
     val command_reports = Outer_Syntax.command_reports thy;
 
-    val proper_range = Token.range_of (drop_suffix Token.is_improper span);
+    val core_range = Token.range_of (drop_suffix Token.is_ignored span);
     val pos =
       (case find_first Token.is_command span of
         SOME tok => Token.pos_of tok
-      | NONE => #1 proper_range);
+      | NONE => #1 core_range);
 
     val token_reports = map (reports_of_token keywords) span;
     val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
@@ -150,8 +150,8 @@
       (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
         [tr] => Toplevel.modify_init init tr
       | [] => Toplevel.ignored (#1 (Token.range_of span))
-      | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
-      handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
+      | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
+      handle ERROR msg => Toplevel.malformed (#1 core_range) msg
   end;
 
 end;
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -319,7 +319,7 @@
               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 @@
 
                 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 @@
   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)
 
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -1024,7 +1024,7 @@
             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) {
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -587,36 +587,6 @@
         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 @@
         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 @@
         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
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/Tools/build.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -64,15 +64,16 @@
       }
     }
 
-    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 @@
       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 @@
         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 @@
     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)
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Pure/Tools/build_docker.scala
--- a/src/Pure/Tools/build_docker.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Pure/Tools/build_docker.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -129,9 +129,9 @@
 
   Examples:
 
-    isabelle build_docker -E -t test/isabelle:Isabelle2017 Isabelle2017_app.tar.gz
+    isabelle build_docker -E -t test/isabelle:Isabelle2018 Isabelle2018_app.tar.gz
 
-    isabelle build_docker -E -n -o Dockerfile http://isabelle.in.tum.de/dist/Isabelle2017_app.tar.gz
+    isabelle build_docker -E -n -o Dockerfile http://isabelle.in.tum.de/dist/Isabelle2018_app.tar.gz
 
 """,
           "B:" -> (arg => base = arg),
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -81,7 +81,7 @@
         PIDE.editor.current_command(view, snapshot) match {
           case Some(command) =>
             snapshot.node.command_start(command) match {
-              case Some(start) => List(snapshot.convert(command.proper_range + start))
+              case Some(start) => List(snapshot.convert(command.core_range + start))
               case None => Nil
             }
           case None => Nil
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -334,7 +334,7 @@
           node.command_start(command) match {
             case Some(start) =>
               JEdit_Lib.buffer_edit(buffer) {
-                val range = command.proper_range + start
+                val range = command.core_range + start
                 JEdit_Lib.buffer_edit(buffer) {
                   if (padding) {
                     text_area.moveCaretPosition(start + range.length)
diff -r ec0b2833cfc4 -r 682ff0e84387 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Mon Aug 06 11:06:43 2018 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Sat Aug 11 16:02:55 2018 +0200
@@ -26,13 +26,13 @@
     def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     {
       val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
-      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
+      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
     }
 
     def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     {
       val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
-      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
+      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
     }
   }