--- 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
--- 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
--- 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
--- 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.
--- 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
Binary file src/Doc/JEdit/document/bibtex-mode.png has changed
--- 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
--- 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)
--- 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
--- 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()
--- 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;
--- 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
--- 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;
--- 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)
--- 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) {
--- 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
--- 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)
--- 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),
--- 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
--- 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)
--- 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)
}
}