merged
authorwenzelm
Thu Jan 31 21:59:30 2019 +0100 (3 months ago)
changeset 6977809ad02c0fbee
parent 69768 7e4966eaf781
parent 69777 1df241e340c8
child 69779 a2218981a5d6
merged
NEWS
     1.1 --- a/Admin/components/components.sha1	Thu Jan 31 13:08:59 2019 +0000
     1.2 +++ b/Admin/components/components.sha1	Thu Jan 31 21:59:30 2019 +0100
     1.3 @@ -197,6 +197,7 @@
     1.4  171b5783b88522a35e4822b19ef8ba838c04f494  polyml-5.7.1.tar.gz
     1.5  5fbcab1da2b5eb97f24da2590ece189d55b3a105  polyml-5.7.tar.gz
     1.6  49f1adfacdd6d29fa9f72035d94a31eaac411a97  polyml-test-0a6ebca445fc.tar.gz
     1.7 +2a8c4421e0a03c0d6ad556b3c36c34eb11568adb  polyml-test-1236652ebd55.tar.gz
     1.8  a0064c157a59e2706e18512a49a6dca914fa17fc  polyml-test-1b2dcf8f5202.tar.gz
     1.9  4e6543dbbb2b2aa402fd61428e1c045c48f18b47  polyml-test-79534495ee94.tar.gz
    1.10  853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e  polyml-test-7a7b742897e9.tar.gz
     2.1 --- a/Admin/components/main	Thu Jan 31 13:08:59 2019 +0000
     2.2 +++ b/Admin/components/main	Thu Jan 31 21:59:30 2019 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4  kodkodi-1.5.2-1
     2.5  nunchaku-0.5
     2.6  opam-1.2.2
     2.7 -polyml-test-1b2dcf8f5202
     2.8 +polyml-test-1236652ebd55
     2.9  postgresql-42.2.5
    2.10  scala-2.12.8
    2.11  smbc-0.4.1
     3.1 --- a/Admin/polyml/README	Thu Jan 31 13:08:59 2019 +0000
     3.2 +++ b/Admin/polyml/README	Thu Jan 31 21:59:30 2019 +0100
     3.3 @@ -3,7 +3,7 @@
     3.4  
     3.5  This compilation of Poly/ML (https://www.polyml.org) is based on the
     3.6  repository version
     3.7 -https://github.com/polyml/polyml/commit/1b2dcf8f5202 (master).
     3.8 +https://github.com/polyml/polyml/commit/1236652ebd55 (master).
     3.9  
    3.10  The Isabelle repository provides the administrative tool
    3.11  "build_polyml", which can be used in the polyml component directory as
    3.12 @@ -48,4 +48,4 @@
    3.13  
    3.14  
    3.15          Makarius
    3.16 -        27-Jan-2019
    3.17 +        31-Jan-2019
     4.1 --- a/NEWS	Thu Jan 31 13:08:59 2019 +0000
     4.2 +++ b/NEWS	Thu Jan 31 21:59:30 2019 +0100
     4.3 @@ -53,6 +53,9 @@
     4.4  entries are structured according to chapter / session names, the open
     4.5  operation is redirected to the session ROOT file.
     4.6  
     4.7 +* System option "jedit_text_overview" allows to disable the text
     4.8 +overview column.
     4.9 +
    4.10  * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
    4.11  DejaVu" collection by default, which provides uniform rendering quality
    4.12  with the usual Isabelle symbols. Line spacing no longer needs to be
     5.1 --- a/src/Pure/Tools/build.scala	Thu Jan 31 13:08:59 2019 +0000
     5.2 +++ b/src/Pure/Tools/build.scala	Thu Jan 31 21:59:30 2019 +0100
     5.3 @@ -233,8 +233,7 @@
     5.4              ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
     5.5  
     5.6          def save_heap: String =
     5.7 -          (if (info.theories.isEmpty) ""
     5.8 -           else """cond_timeit true "share_common_data" ML_Heap.share_common_data; """) +
     5.9 +          (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") +
    5.10              "ML_Heap.save_child " +
    5.11              ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name)))
    5.12  
     6.1 --- a/src/Pure/Tools/main.scala	Thu Jan 31 13:08:59 2019 +0000
     6.2 +++ b/src/Pure/Tools/main.scala	Thu Jan 31 21:59:30 2019 +0100
     6.3 @@ -53,13 +53,13 @@
     6.4  
     6.5          if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
     6.6            File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
     6.7 -            """<DOCKING LEFT="vfs.browser" TOP="" RIGHT="isabelle-documentation" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
     6.8 +            """<DOCKING LEFT="isabelle-documentation" TOP="" RIGHT="isabelle-theories" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
     6.9            File.write(settings_dir + Path.explode("perspective.xml"),
    6.10              """<?xml version="1.0" encoding="UTF-8" ?>
    6.11  <!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
    6.12  <PERSPECTIVE>
    6.13  <VIEW PLAIN="FALSE">
    6.14 -<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
    6.15 +<GEOMETRY X="0" Y="35" WIDTH="1200" HEIGHT="850" EXT_STATE="0" />
    6.16  </VIEW>
    6.17  </PERSPECTIVE>""")
    6.18          }
     7.1 --- a/src/Pure/library.ML	Thu Jan 31 13:08:59 2019 +0000
     7.2 +++ b/src/Pure/library.ML	Thu Jan 31 21:59:30 2019 +0100
     7.3 @@ -251,8 +251,8 @@
     7.4  fun (f oooo g) x y z w = f (g x y z w);
     7.5  
     7.6  (*function exponentiation: f (... (f x) ...) with n applications of f*)
     7.7 -fun funpow (0 : int) _ = I
     7.8 -  | funpow n f = f #> funpow (n - 1) f;
     7.9 +fun funpow (0: int) _ x = x
    7.10 +  | funpow n f x = funpow (n - 1) f (f x);
    7.11  
    7.12  fun funpow_yield (0 : int) _ x = ([], x)
    7.13    | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
     8.1 --- a/src/Tools/jEdit/etc/options	Thu Jan 31 13:08:59 2019 +0000
     8.2 +++ b/src/Tools/jEdit/etc/options	Thu Jan 31 21:59:30 2019 +0100
     8.3 @@ -36,6 +36,9 @@
     8.4  public option jedit_timing_threshold : real = 0.1
     8.5    -- "default threshold for timing display (seconds)"
     8.6  
     8.7 +public option jedit_text_overview : bool = true
     8.8 +  -- "paint text overview column"
     8.9 +
    8.10  
    8.11  section "Indentation"
    8.12  
     9.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Jan 31 13:08:59 2019 +0000
     9.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Jan 31 21:59:30 2019 +0100
     9.3 @@ -196,7 +196,8 @@
     9.4  
     9.5    /* text status overview left of scrollbar */
     9.6  
     9.7 -  private val text_overview = new Text_Overview(this)
     9.8 +  private val text_overview: Option[Text_Overview] =
     9.9 +    if (PIDE.options.bool("jedit_text_overview")) Some(new Text_Overview(this)) else None
    9.10  
    9.11  
    9.12    /* main */
    9.13 @@ -204,7 +205,7 @@
    9.14    private val main =
    9.15      Session.Consumer[Any](getClass.getName) {
    9.16        case _: Session.Raw_Edits =>
    9.17 -        text_overview.invoke()
    9.18 +        text_overview.foreach(_.invoke())
    9.19  
    9.20        case changed: Session.Commands_Changed =>
    9.21          val buffer = model.buffer
    9.22 @@ -216,7 +217,7 @@
    9.23                if (changed.assignment ||
    9.24                    (changed.nodes.contains(model.node_name) &&
    9.25                     changed.commands.exists(snapshot.node.commands.contains)))
    9.26 -                text_overview.invoke()
    9.27 +                text_overview.foreach(_.invoke())
    9.28  
    9.29                JEdit_Lib.invalidate(text_area)
    9.30              }
    9.31 @@ -236,7 +237,9 @@
    9.32      text_area.getGutter.addExtension(gutter_painter)
    9.33      text_area.addKeyListener(key_listener)
    9.34      text_area.addCaretListener(caret_listener)
    9.35 -    text_area.addLeftOfScrollBar(text_overview); text_area.revalidate(); text_area.repaint()
    9.36 +    text_overview.foreach(text_area.addLeftOfScrollBar(_))
    9.37 +    text_area.revalidate()
    9.38 +    text_area.repaint()
    9.39      Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
    9.40        foreach(text_area.addStructureMatcher(_))
    9.41      session.raw_edits += main
    9.42 @@ -251,8 +254,10 @@
    9.43      session.commands_changed -= main
    9.44      Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
    9.45        foreach(text_area.removeStructureMatcher(_))
    9.46 -    text_overview.revoke(); text_area.removeLeftOfScrollBar(text_overview)
    9.47 -    text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
    9.48 +    text_overview.foreach(_.revoke())
    9.49 +    text_overview.foreach(text_area.removeLeftOfScrollBar(_))
    9.50 +    text_area.removeCaretListener(caret_listener)
    9.51 +    delay_caret_update.revoke()
    9.52      text_area.removeKeyListener(key_listener)
    9.53      text_area.getGutter.removeExtension(gutter_painter)
    9.54      rich_text_area.deactivate()
    10.1 --- a/src/Tools/jEdit/src/jEdit.props	Thu Jan 31 13:08:59 2019 +0000
    10.2 +++ b/src/Tools/jEdit/src/jEdit.props	Thu Jan 31 21:59:30 2019 +0100
    10.3 @@ -187,18 +187,20 @@
    10.4  home.shortcut=
    10.5  insert-newline-indent.shortcut=
    10.6  insert-newline.shortcut=
    10.7 -isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
    10.8  isabelle-debugger.dock-position=floating
    10.9 -isabelle-documentation.dock-position=right
   10.10 +isabelle-documentation.dock-position=left
   10.11 +isabelle-export-browser.label=Browse theory exports
   10.12  isabelle-output.dock-position=bottom
   10.13  isabelle-output.height=174
   10.14  isabelle-output.width=412
   10.15  isabelle-query.dock-position=bottom
   10.16 +isabelle-session-browser.label=Browse session information
   10.17  isabelle-simplifier-trace.dock-position=floating
   10.18  isabelle-sledgehammer.dock-position=bottom
   10.19  isabelle-state.dock-position=right
   10.20  isabelle-symbols.dock-position=bottom
   10.21  isabelle-theories.dock-position=right
   10.22 +isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
   10.23  isabelle.complete-word.label=Complete word
   10.24  isabelle.complete.label=Complete Isabelle text
   10.25  isabelle.complete.shortcut2=C+b
   10.26 @@ -230,8 +232,6 @@
   10.27  isabelle.newline.shortcut=ENTER
   10.28  isabelle.options.label=Isabelle options
   10.29  isabelle.preview.label=Show preview in browser
   10.30 -isabelle-export-browser.label=Browse theory exports
   10.31 -isabelle-session-browser.label=Browse session information
   10.32  isabelle.reset-continuous-checking.label=Reset continuous checking
   10.33  isabelle.reset-font-size.label=Reset font size
   10.34  isabelle.reset-node-required.label=Reset node required
   10.35 @@ -290,6 +290,7 @@
   10.36  toggle-multi-select.shortcut2=C+NUMBER_SIGN
   10.37  toggle-rect-select.shortcut2=A+NUMBER_SIGN
   10.38  twoStageSave=false
   10.39 +vfs.browser.defaultPath=favorites
   10.40  vfs.browser.dock-position=left
   10.41  vfs.favorite.0.type=1
   10.42  vfs.favorite.0=$ISABELLE_HOME
   10.43 @@ -316,9 +317,9 @@
   10.44  view.gutter.fontsize=12
   10.45  view.gutter.lineNumbers=false
   10.46  view.gutter.selectionAreaWidth=18
   10.47 -view.height=787
   10.48 +view.height=850
   10.49  view.middleMousePaste=true
   10.50  view.showToolbar=true
   10.51  view.thickCaret=true
   10.52 -view.width=1072
   10.53 +view.width=1200
   10.54  xml-insert-closing-tag.shortcut=