--- a/Admin/components/components.sha1 Thu Jan 31 13:08:59 2019 +0000
+++ b/Admin/components/components.sha1 Thu Jan 31 21:59:30 2019 +0100
@@ -197,6 +197,7 @@
171b5783b88522a35e4822b19ef8ba838c04f494 polyml-5.7.1.tar.gz
5fbcab1da2b5eb97f24da2590ece189d55b3a105 polyml-5.7.tar.gz
49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz
+2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz
a0064c157a59e2706e18512a49a6dca914fa17fc polyml-test-1b2dcf8f5202.tar.gz
4e6543dbbb2b2aa402fd61428e1c045c48f18b47 polyml-test-79534495ee94.tar.gz
853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz
--- a/Admin/components/main Thu Jan 31 13:08:59 2019 +0000
+++ b/Admin/components/main Thu Jan 31 21:59:30 2019 +0100
@@ -12,7 +12,7 @@
kodkodi-1.5.2-1
nunchaku-0.5
opam-1.2.2
-polyml-test-1b2dcf8f5202
+polyml-test-1236652ebd55
postgresql-42.2.5
scala-2.12.8
smbc-0.4.1
--- a/Admin/polyml/README Thu Jan 31 13:08:59 2019 +0000
+++ b/Admin/polyml/README Thu Jan 31 21:59:30 2019 +0100
@@ -3,7 +3,7 @@
This compilation of Poly/ML (https://www.polyml.org) is based on the
repository version
-https://github.com/polyml/polyml/commit/1b2dcf8f5202 (master).
+https://github.com/polyml/polyml/commit/1236652ebd55 (master).
The Isabelle repository provides the administrative tool
"build_polyml", which can be used in the polyml component directory as
@@ -48,4 +48,4 @@
Makarius
- 27-Jan-2019
+ 31-Jan-2019
--- a/NEWS Thu Jan 31 13:08:59 2019 +0000
+++ b/NEWS Thu Jan 31 21:59:30 2019 +0100
@@ -53,6 +53,9 @@
entries are structured according to chapter / session names, the open
operation is redirected to the session ROOT file.
+* System option "jedit_text_overview" allows to disable the text
+overview column.
+
* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
DejaVu" collection by default, which provides uniform rendering quality
with the usual Isabelle symbols. Line spacing no longer needs to be
--- a/src/Pure/Tools/build.scala Thu Jan 31 13:08:59 2019 +0000
+++ b/src/Pure/Tools/build.scala Thu Jan 31 21:59:30 2019 +0100
@@ -233,8 +233,7 @@
("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
def save_heap: String =
- (if (info.theories.isEmpty) ""
- else """cond_timeit true "share_common_data" ML_Heap.share_common_data; """) +
+ (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") +
"ML_Heap.save_child " +
ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name)))
--- a/src/Pure/Tools/main.scala Thu Jan 31 13:08:59 2019 +0000
+++ b/src/Pure/Tools/main.scala Thu Jan 31 21:59:30 2019 +0100
@@ -53,13 +53,13 @@
if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
- """<DOCKING LEFT="vfs.browser" TOP="" RIGHT="isabelle-documentation" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
+ """<DOCKING LEFT="isabelle-documentation" TOP="" RIGHT="isabelle-theories" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
File.write(settings_dir + Path.explode("perspective.xml"),
"""<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
<PERSPECTIVE>
<VIEW PLAIN="FALSE">
-<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
+<GEOMETRY X="0" Y="35" WIDTH="1200" HEIGHT="850" EXT_STATE="0" />
</VIEW>
</PERSPECTIVE>""")
}
--- a/src/Pure/library.ML Thu Jan 31 13:08:59 2019 +0000
+++ b/src/Pure/library.ML Thu Jan 31 21:59:30 2019 +0100
@@ -251,8 +251,8 @@
fun (f oooo g) x y z w = f (g x y z w);
(*function exponentiation: f (... (f x) ...) with n applications of f*)
-fun funpow (0 : int) _ = I
- | funpow n f = f #> funpow (n - 1) f;
+fun funpow (0: int) _ x = x
+ | funpow n f x = funpow (n - 1) f (f x);
fun funpow_yield (0 : int) _ x = ([], x)
| funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
--- a/src/Tools/jEdit/etc/options Thu Jan 31 13:08:59 2019 +0000
+++ b/src/Tools/jEdit/etc/options Thu Jan 31 21:59:30 2019 +0100
@@ -36,6 +36,9 @@
public option jedit_timing_threshold : real = 0.1
-- "default threshold for timing display (seconds)"
+public option jedit_text_overview : bool = true
+ -- "paint text overview column"
+
section "Indentation"
--- a/src/Tools/jEdit/src/document_view.scala Thu Jan 31 13:08:59 2019 +0000
+++ b/src/Tools/jEdit/src/document_view.scala Thu Jan 31 21:59:30 2019 +0100
@@ -196,7 +196,8 @@
/* text status overview left of scrollbar */
- private val text_overview = new Text_Overview(this)
+ private val text_overview: Option[Text_Overview] =
+ if (PIDE.options.bool("jedit_text_overview")) Some(new Text_Overview(this)) else None
/* main */
@@ -204,7 +205,7 @@
private val main =
Session.Consumer[Any](getClass.getName) {
case _: Session.Raw_Edits =>
- text_overview.invoke()
+ text_overview.foreach(_.invoke())
case changed: Session.Commands_Changed =>
val buffer = model.buffer
@@ -216,7 +217,7 @@
if (changed.assignment ||
(changed.nodes.contains(model.node_name) &&
changed.commands.exists(snapshot.node.commands.contains)))
- text_overview.invoke()
+ text_overview.foreach(_.invoke())
JEdit_Lib.invalidate(text_area)
}
@@ -236,7 +237,9 @@
text_area.getGutter.addExtension(gutter_painter)
text_area.addKeyListener(key_listener)
text_area.addCaretListener(caret_listener)
- text_area.addLeftOfScrollBar(text_overview); text_area.revalidate(); text_area.repaint()
+ text_overview.foreach(text_area.addLeftOfScrollBar(_))
+ text_area.revalidate()
+ text_area.repaint()
Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
foreach(text_area.addStructureMatcher(_))
session.raw_edits += main
@@ -251,8 +254,10 @@
session.commands_changed -= main
Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
foreach(text_area.removeStructureMatcher(_))
- text_overview.revoke(); text_area.removeLeftOfScrollBar(text_overview)
- text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
+ text_overview.foreach(_.revoke())
+ text_overview.foreach(text_area.removeLeftOfScrollBar(_))
+ text_area.removeCaretListener(caret_listener)
+ delay_caret_update.revoke()
text_area.removeKeyListener(key_listener)
text_area.getGutter.removeExtension(gutter_painter)
rich_text_area.deactivate()
--- a/src/Tools/jEdit/src/jEdit.props Thu Jan 31 13:08:59 2019 +0000
+++ b/src/Tools/jEdit/src/jEdit.props Thu Jan 31 21:59:30 2019 +0100
@@ -187,18 +187,20 @@
home.shortcut=
insert-newline-indent.shortcut=
insert-newline.shortcut=
-isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
isabelle-debugger.dock-position=floating
-isabelle-documentation.dock-position=right
+isabelle-documentation.dock-position=left
+isabelle-export-browser.label=Browse theory exports
isabelle-output.dock-position=bottom
isabelle-output.height=174
isabelle-output.width=412
isabelle-query.dock-position=bottom
+isabelle-session-browser.label=Browse session information
isabelle-simplifier-trace.dock-position=floating
isabelle-sledgehammer.dock-position=bottom
isabelle-state.dock-position=right
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
+isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
isabelle.complete-word.label=Complete word
isabelle.complete.label=Complete Isabelle text
isabelle.complete.shortcut2=C+b
@@ -230,8 +232,6 @@
isabelle.newline.shortcut=ENTER
isabelle.options.label=Isabelle options
isabelle.preview.label=Show preview in browser
-isabelle-export-browser.label=Browse theory exports
-isabelle-session-browser.label=Browse session information
isabelle.reset-continuous-checking.label=Reset continuous checking
isabelle.reset-font-size.label=Reset font size
isabelle.reset-node-required.label=Reset node required
@@ -290,6 +290,7 @@
toggle-multi-select.shortcut2=C+NUMBER_SIGN
toggle-rect-select.shortcut2=A+NUMBER_SIGN
twoStageSave=false
+vfs.browser.defaultPath=favorites
vfs.browser.dock-position=left
vfs.favorite.0.type=1
vfs.favorite.0=$ISABELLE_HOME
@@ -316,9 +317,9 @@
view.gutter.fontsize=12
view.gutter.lineNumbers=false
view.gutter.selectionAreaWidth=18
-view.height=787
+view.height=850
view.middleMousePaste=true
view.showToolbar=true
view.thickCaret=true
-view.width=1072
+view.width=1200
xml-insert-closing-tag.shortcut=