# HG changeset patch # User wenzelm # Date 1540503847 -7200 # Node ID 278b09a92ed6f05a559beb1493bd76284c49f83f # Parent 91fd09f2b86e8c814885a08b054c15fceeefb1fb# Parent f714114b05713e0ef909ce87f9119631eb46df2b merged diff -r 91fd09f2b86e -r 278b09a92ed6 Admin/components/components.sha1 --- 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 diff -r 91fd09f2b86e -r 278b09a92ed6 Admin/components/main --- 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 diff -r 91fd09f2b86e -r 278b09a92ed6 NEWS --- 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. diff -r 91fd09f2b86e -r 278b09a92ed6 src/HOL/ex/Cartouche_Examples.thy --- 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; diff -r 91fd09f2b86e -r 278b09a92ed6 src/Pure/Admin/build_jdk.scala --- 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 = diff -r 91fd09f2b86e -r 278b09a92ed6 src/Pure/General/name_space.ML --- 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))) diff -r 91fd09f2b86e -r 278b09a92ed6 src/Pure/Isar/attrib.ML --- 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; diff -r 91fd09f2b86e -r 278b09a92ed6 src/Pure/Isar/isar_cmd.ML --- 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) ^ diff -r 91fd09f2b86e -r 278b09a92ed6 src/Pure/Isar/method.ML --- 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; diff -r 91fd09f2b86e -r 278b09a92ed6 src/Pure/Isar/proof_context.ML --- 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; diff -r 91fd09f2b86e -r 278b09a92ed6 src/Pure/ML/ml_context.ML --- 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 ())));"))); diff -r 91fd09f2b86e -r 278b09a92ed6 src/Pure/Tools/main.scala --- 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") - } - } } diff -r 91fd09f2b86e -r 278b09a92ed6 src/Pure/Tools/named_theorems.ML --- 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; diff -r 91fd09f2b86e -r 278b09a92ed6 src/Tools/jEdit/patches/putenv --- /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 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) {