--- a/Admin/components/components.sha1 Thu Oct 25 12:42:17 2018 +0000
+++ b/Admin/components/components.sha1 Thu Oct 25 23:44:07 2018 +0200
@@ -70,6 +70,7 @@
b70690c85c05d0ca5bc29287abd20142f6ddcfb0 isabelle_fonts-20171222.tar.gz
c17c482e411bbaf992498041a3e1dea80336aaa6 isabelle_fonts-20171230.tar.gz
3affbb306baff37c360319b21cbaa2cc96ebb282 isabelle_fonts-20180113.tar.gz
+0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
71d19df63816e9be1c4c5eb44aea7a44cfadb319 jdk-11.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
@@ -133,6 +134,7 @@
d806c1c26b571b5b4ef05ea11e8b9cf936518e06 jedit_build-20170319.tar.gz
7bcb202e13358dd750e964b2f747664428b5d8b3 jedit_build-20180417.tar.gz
23c8a05687d05a6937f7d600ac3aa19e3ce59c9c jedit_build-20180504.tar.gz
+9c64ee0705e5284b507ca527196081979d689519 jedit_build-20181025.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
--- a/Admin/components/main Thu Oct 25 12:42:17 2018 +0000
+++ b/Admin/components/main Thu Oct 25 23:44:07 2018 +0200
@@ -5,8 +5,8 @@
cvc4-1.5-4
e-2.0-2
isabelle_fonts-20180113
-jdk-8u181
-jedit_build-20180504
+jdk-11+28
+jedit_build-20181025
jfreechart-1.5.0
jortho-1.0-2
kodkodi-1.5.2-1
--- a/NEWS Thu Oct 25 12:42:17 2018 +0000
+++ b/NEWS Thu Oct 25 23:44:07 2018 +0200
@@ -16,6 +16,12 @@
without additional spaces, eg "(*)" instead of "( * )".
+*** Isabelle/jEdit Prover IDE ***
+
+* Improved sub-pixel font rendering (especially on Linux), thanks to
+OpenJDK 11.
+
+
*** Isar ***
* More robust treatment of structural errors: begin/end blocks take
@@ -101,7 +107,10 @@
* Support for Glasgow Haskell Compiler via command-line tools "isabelle
ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
Existing settings variable ISABELLE_GHC is maintained dynamically
-according to the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
+according to the state of ISABELLE_STACK_ROOT and
+ISABELLE_STACK_RESOLVER.
+
+* Update to Java 11: the latest long-term support version of OpenJDK.
--- a/src/HOL/ex/Cartouche_Examples.thy Thu Oct 25 12:42:17 2018 +0000
+++ b/src/HOL/ex/Cartouche_Examples.thy Thu Oct 25 23:44:07 2018 +0200
@@ -176,7 +176,7 @@
fun ml_tactic source ctxt =
let
val ctxt' = ctxt |> Context.proof_map
- (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
+ (ML_Context.expression ("tactic", Position.thread_data ()) "Proof.context -> tactic"
"Context.map_proof (ML_Tactic.set tactic)"
(ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source source));
in Data.get ctxt' ctxt end;
--- a/src/Pure/Admin/build_jdk.scala Thu Oct 25 12:42:17 2018 +0000
+++ b/src/Pure/Admin/build_jdk.scala Thu Oct 25 23:44:07 2018 +0200
@@ -7,6 +7,7 @@
package isabelle
+import java.io.{File => JFile}
import java.nio.file.Files
import java.nio.file.attribute.PosixFilePermission
@@ -19,7 +20,7 @@
def detect_version(s: String): String =
{
- val Version_Dir_Entry = """^jdk-(\d+)(?:\.jdk)?$""".r
+ val Version_Dir_Entry = """^jdk-(\d+\+\d+)$""".r
s match {
case Version_Dir_Entry(version) => version
case _ => error("Cannot detect JDK version from " + quote(s))
@@ -56,7 +57,7 @@
def readme(version: String): String =
"""This is OpenJDK """ + version + """ as required for Isabelle.
-See http://jdk.java.net for the original downloads, which are covered
+See https://adoptopenjdk.net for the original downloads, which are covered
the GPL2 (with various liberal exceptions, see legal/*).
Linux, Windows, Mac OS X all work uniformly, depending on certain
@@ -88,6 +89,8 @@
/* extract archive */
+ private def suppress_name(name: String): Boolean = name.startsWith("._")
+
def extract_archive(dir: Path, archive: Path): (String, JDK_Platform) =
{
try {
@@ -104,7 +107,7 @@
}
val dir_entry =
- File.read_dir(tmp_dir) match {
+ File.read_dir(tmp_dir).filterNot(suppress_name(_)) match {
case List(s) => s
case _ => error("Archive contains multiple directories")
}
@@ -183,7 +186,7 @@
}
File.find_files((component_dir + Path.explode("x86_64-darwin")).file,
- file => file.getName.startsWith("._")).foreach(_.delete)
+ file => suppress_name(file.getName)).foreach(_.delete)
progress.echo("Sharing ...")
val main_dir :: other_dirs =
--- a/src/Pure/General/name_space.ML Thu Oct 25 12:42:17 2018 +0000
+++ b/src/Pure/General/name_space.ML Thu Oct 25 23:44:07 2018 +0200
@@ -30,7 +30,7 @@
val extern_shortest: Proof.context -> T -> string -> xstring
val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
val pretty: Proof.context -> T -> string -> Pretty.T
- val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
+ val completion: Context.generic -> T -> (string -> bool) -> xstring * Position.T -> Completion.T
val merge: T * T -> T
type naming
val get_scopes: naming -> Binding.scope list
@@ -257,7 +257,7 @@
(* completion *)
-fun completion context space (xname, pos) =
+fun completion context space pred (xname, pos) =
Completion.make (xname, pos) (fn completed =>
let
fun result_ord ((pri1, (xname1, (_, name1))), (pri2, (xname2, (_, name2)))) =
@@ -276,7 +276,7 @@
fun complete xname' name =
if (completed xname' orelse exists completed (Long_Name.explode xname')) andalso
- not (is_concealed space name)
+ not (is_concealed space name) andalso pred name
then
let
val xname'' = ext name;
@@ -565,7 +565,7 @@
in ((name, reports), x) end
| NONE =>
let
- val completions = map (fn pos => completion context space (xname, pos)) ps;
+ val completions = map (fn pos => completion context space (K true) (xname, pos)) ps;
in
error (undefined space name ^ Position.here_list ps ^
Markup.markup_report (implode (map Completion.reported_text completions)))
--- a/src/Pure/Isar/attrib.ML Thu Oct 25 12:42:17 2018 +0000
+++ b/src/Pure/Isar/attrib.ML Thu Oct 25 23:44:07 2018 +0200
@@ -214,10 +214,11 @@
fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
-fun attribute_setup name source comment =
+fun attribute_setup (name, pos) source comment =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser"
- ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
+ |> ML_Context.expression ("parser", pos) "Thm.attribute context_parser"
+ ("Context.map_proof (Attrib.local_setup " ^
+ ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
" parser " ^ ML_Syntax.print_string comment ^ ")")
|> Context.proof_map;
--- a/src/Pure/Isar/isar_cmd.ML Thu Oct 25 12:42:17 2018 +0000
+++ b/src/Pure/Isar/isar_cmd.ML Thu Oct 25 23:44:07 2018 +0200
@@ -52,13 +52,13 @@
fun setup source =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
+ |> ML_Context.expression ("setup", Position.thread_data ()) "theory -> theory"
"Context.map_theory setup"
|> Context.theory_map;
fun local_setup source =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
+ |> ML_Context.expression ("local_setup", Position.thread_data ()) "local_theory -> local_theory"
"Context.map_proof local_setup"
|> Context.proof_map;
@@ -67,35 +67,35 @@
fun parse_ast_translation source =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "parse_ast_translation"
+ |> ML_Context.expression ("parse_ast_translation", Position.thread_data ())
"(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
|> Context.theory_map;
fun parse_translation source =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "parse_translation"
+ |> ML_Context.expression ("parse_translation", Position.thread_data ())
"(string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.parse_translation parse_translation)"
|> Context.theory_map;
fun print_translation source =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "print_translation"
+ |> ML_Context.expression ("print_translation", Position.thread_data ())
"(string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.print_translation print_translation)"
|> Context.theory_map;
fun typed_print_translation source =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "typed_print_translation"
+ |> ML_Context.expression ("typed_print_translation", Position.thread_data ())
"(string * (Proof.context -> typ -> term list -> term)) list"
"Context.map_theory (Sign.typed_print_translation typed_print_translation)"
|> Context.theory_map;
fun print_ast_translation source =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "print_ast_translation"
+ |> ML_Context.expression ("print_ast_translation", Position.thread_data ())
"(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.print_ast_translation print_ast_translation)"
|> Context.theory_map;
@@ -143,7 +143,7 @@
fun declaration {syntax, pervasive} source =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
+ |> ML_Context.expression ("declaration", Position.thread_data ()) "Morphism.declaration"
("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
\pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
|> Context.proof_map;
@@ -153,7 +153,7 @@
fun simproc_setup name lhss source =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "proc"
+ |> ML_Context.expression ("proc", Position.thread_data ())
"Morphism.morphism -> Proof.context -> cterm -> thm option"
("Context.map_proof (Simplifier.define_simproc_cmd " ^
ML_Syntax.atomic (ML_Syntax.make_binding name) ^
--- a/src/Pure/Isar/method.ML Thu Oct 25 12:42:17 2018 +0000
+++ b/src/Pure/Isar/method.ML Thu Oct 25 23:44:07 2018 +0200
@@ -369,8 +369,8 @@
Scan.lift (Args.text_declaration (fn source =>
let
val context' = context |>
- ML_Context.expression (Input.range_of source)
- "tactic" "Morphism.morphism -> thm list -> tactic"
+ ML_Context.expression ("tactic", Position.thread_data ())
+ "Morphism.morphism -> thm list -> tactic"
"Method.set_tactic tactic"
(ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @
ML_Lex.read_source source);
@@ -475,11 +475,12 @@
fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
-fun method_setup name source comment =
+fun method_setup (name, pos) source comment =
ML_Lex.read_source source
- |> ML_Context.expression (Input.range_of source) "parser"
+ |> ML_Context.expression ("parser", pos)
"(Proof.context -> Proof.method) context_parser"
- ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
+ ("Context.map_proof (Method.local_setup " ^
+ ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
" parser " ^ ML_Syntax.print_string comment ^ ")")
|> Context.proof_map;
--- a/src/Pure/Isar/proof_context.ML Thu Oct 25 12:42:17 2018 +0000
+++ b/src/Pure/Isar/proof_context.ML Thu Oct 25 23:44:07 2018 +0200
@@ -451,7 +451,7 @@
handle TYPE (msg, _, _) =>
error (msg ^ Position.here pos ^
Markup.markup_report (Completion.reported_text
- (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
+ (Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos))));
val reports =
if Context_Position.is_reported ctxt pos
then [(pos, Name_Space.markup class_space name)] else [];
@@ -535,7 +535,7 @@
fun consts_completion_message ctxt (c, ps) =
ps |> map (fn pos =>
- Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (c, pos)
+ Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos)
|> Completion.reported_text)
|> implode
|> Markup.markup_report;
--- a/src/Pure/ML/ml_context.ML Thu Oct 25 12:42:17 2018 +0000
+++ b/src/Pure/ML/ml_context.ML Thu Oct 25 23:44:07 2018 +0200
@@ -21,7 +21,7 @@
ML_Lex.token Antiquote.antiquote list -> unit
val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
val exec: (unit -> unit) -> Context.generic -> Context.generic
- val expression: Position.range -> string -> string -> string ->
+ val expression: string * Position.T -> string -> string ->
ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
end
@@ -214,10 +214,11 @@
SOME context' => context'
| NONE => error "Missing context after execution");
-fun expression range name constraint body ants =
+fun expression (name, pos) constraint body ants =
exec (fn () =>
- eval ML_Compiler.flags (#1 range)
- (ML_Lex.read "Context.put_generic_context (SOME (let val " @ ML_Lex.read_set_range range name @
+ eval ML_Compiler.flags pos
+ (ML_Lex.read "Context.put_generic_context (SOME (let val " @
+ ML_Lex.read_set_range (Position.range_of_properties (Position.properties_of pos)) name @
ML_Lex.read (": " ^ constraint ^ " =") @ ants @
ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
--- a/src/Pure/Tools/main.scala Thu Oct 25 12:42:17 2018 +0000
+++ b/src/Pure/Tools/main.scala Thu Oct 25 23:44:07 2018 +0200
@@ -90,14 +90,31 @@
}
- /* main startup */
+ /* environment */
- update_environment()
+ def putenv(name: String, value: String)
+ {
+ val misc =
+ Class.forName("org.gjt.sp.jedit.MiscUtilities", true, ClassLoader.getSystemClassLoader)
+ val putenv = misc.getMethod("putenv", classOf[String], classOf[String])
+ putenv.invoke(null, name, value)
+ }
+
+ for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) {
+ putenv(name, File.platform_path(Isabelle_System.getenv(name)))
+ }
+ putenv("ISABELLE_ROOT", null)
+
+
+ /* properties */
System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
System.setProperty("scala.color", "false")
+
+ /* main startup */
+
val jedit =
Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
val jedit_main = jedit.getMethod("main", classOf[Array[String]])
@@ -114,46 +131,4 @@
}
start()
}
-
-
- /* adhoc update of JVM environment variables */
-
- def update_environment()
- {
- val update =
- {
- val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
- val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER")
- val jedit_home = Isabelle_System.getenv("JEDIT_HOME")
- val jedit_settings = Isabelle_System.getenv("JEDIT_SETTINGS")
-
- (env0: Any) => {
- val env = env0.asInstanceOf[java.util.Map[String, String]]
- env.put("ISABELLE_HOME", File.platform_path(isabelle_home))
- env.put("ISABELLE_HOME_USER", File.platform_path(isabelle_home_user))
- env.put("JEDIT_HOME", File.platform_path(jedit_home))
- env.put("JEDIT_SETTINGS", File.platform_path(jedit_settings))
- env.remove("ISABELLE_ROOT")
- }
- }
-
- classOf[java.util.Collections].getDeclaredClasses
- .find(c => c.getName == "java.util.Collections$UnmodifiableMap") match
- {
- case Some(c) =>
- val m = c.getDeclaredField("m")
- m.setAccessible(true)
- update(m.get(System.getenv()))
-
- if (Platform.is_windows) {
- val ProcessEnvironment = Class.forName("java.lang.ProcessEnvironment")
- val field = ProcessEnvironment.getDeclaredField("theCaseInsensitiveEnvironment")
- field.setAccessible(true)
- update(field.get(null))
- }
-
- case None =>
- error("Failed to update JVM environment -- platform incompatibility")
- }
- }
}
--- a/src/Pure/Tools/named_theorems.ML Thu Oct 25 12:42:17 2018 +0000
+++ b/src/Pure/Tools/named_theorems.ML Thu Oct 25 23:44:07 2018 +0200
@@ -38,6 +38,8 @@
fun undeclared name = "Undeclared named theorems " ^ quote name;
+val defined_entry = Symtab.defined o Data.get;
+
fun the_entry context name =
(case Symtab.lookup (Data.get context) name of
NONE => error (undeclared name)
@@ -71,10 +73,17 @@
let
val context = Context.Proof ctxt;
val fact_ref = Facts.Named ((xname, Position.none), NONE);
- fun err () = error (undeclared xname ^ Position.here pos);
+ fun err () =
+ let
+ val space = Facts.space_of (Proof_Context.facts_of ctxt);
+ val completion = Name_Space.completion context space (defined_entry context) (xname, pos);
+ in
+ error (undeclared xname ^ Position.here pos ^
+ Markup.markup_report (Completion.reported_text completion))
+ end;
in
(case try (Proof_Context.get_fact_generic context) fact_ref of
- SOME (SOME name, _) => if can (the_entry context) name then name else err ()
+ SOME (SOME name, _) => if defined_entry context name then name else err ()
| _ => err ())
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/putenv Thu Oct 25 23:44:07 2018 +0200
@@ -0,0 +1,51 @@
+diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
+--- 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2018-04-09 01:57:06.000000000 +0200
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2018-10-25 22:06:22.258705636 +0200
+@@ -126,6 +126,20 @@
+ static final Pattern winPattern = Pattern.compile(winPatternString);
+
+
++ private static Map<String,String> environ =
++ Collections.synchronizedMap(new HashMap(System.getenv()));
++
++ public static String getenv(String varName)
++ {
++ return environ.get(varName);
++ }
++
++ public static void putenv(String varName, String value)
++ {
++ environ.put(varName, value);
++ }
++
++
+ /** A helper function for expandVariables when handling Windows paths on non-windows systems.
+ */
+ private static String win2unix(String winPath)
+@@ -135,7 +149,7 @@
+ if (m.find())
+ {
+ String varName = m.group(2);
+- String expansion = System.getenv(varName);
++ String expansion = getenv(varName);
+ if (expansion != null)
+ return m.replaceFirst(expansion);
+ }
+@@ -174,7 +188,7 @@
+ return arg;
+ }
+ String varName = m.group(2);
+- String expansion = System.getenv(varName);
++ String expansion = getenv(varName);
+ if (expansion == null) {
+ if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
+ expansion = jEdit.getSettingsDirectory();
+@@ -184,7 +198,7 @@
+ varName = varName.toUpperCase();
+ String uparg = arg.toUpperCase();
+ m = p.matcher(uparg);
+- expansion = System.getenv(varName);
++ expansion = getenv(varName);
+ }
+ }
+ if (expansion != null) {