# HG changeset patch
# User wenzelm
# Date 1516736598 -3600
# Node ID b8e093f7a802e463efe8228975faadacd2596284
# Parent  f1ba59ddd9a6d74251c636f527ad52cca4ee6e7b# Parent  c4e9e0c50487075f296a1bef1f5cf628cc1b459d
merged

diff -r f1ba59ddd9a6 -r b8e093f7a802 Admin/Linux/Isabelle.run
--- a/Admin/Linux/Isabelle.run	Tue Jan 23 12:28:46 2018 +0100
+++ b/Admin/Linux/Isabelle.run	Tue Jan 23 20:43:18 2018 +0100
@@ -20,11 +20,7 @@
 # Java runtime options
 
 ISABELLE_NAME="$(basename "$0" .run)"
-if [ -z "$ISABELLE_PLATFORM64" ]; then
-  declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options32"))
-else
-  declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options64"))
-fi
+declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options"))
 
 
 # main
@@ -32,8 +28,9 @@
 #paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
 unset XMODIFIERS
 
-exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/jre/bin/java" \
+exec "$ISABELLE_HOME/contrib/jdk/x86_64-linux/jre/bin/java" \
   "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
+  "-Djava.ext.dirs=$ISABELLE_HOME/contrib/jdk/x86_64-linux/jre/lib/ext" \
   -classpath "{CLASSPATH}" \
   "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
   isabelle.Main "$@"
diff -r f1ba59ddd9a6 -r b8e093f7a802 Admin/MacOS/Info.plist-part2
--- a/Admin/MacOS/Info.plist-part2	Tue Jan 23 12:28:46 2018 +0100
+++ b/Admin/MacOS/Info.plist-part2	Tue Jan 23 20:43:18 2018 +0100
@@ -1,4 +1,5 @@
 <string>-Disabelle.root=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string>
+<string>-Djava.ext.dirs=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}/contrib/jdk/x86_64-darwin/Contents/Home/jre/lib/ext</string>
 <string>-Disabelle.app=true</string>
 </array>
 <key>JVMArguments</key>
diff -r f1ba59ddd9a6 -r b8e093f7a802 Admin/Windows/launch4j/isabelle.xml
--- a/Admin/Windows/launch4j/isabelle.xml	Tue Jan 23 12:28:46 2018 +0100
+++ b/Admin/Windows/launch4j/isabelle.xml	Tue Jan 23 20:43:18 2018 +0100
@@ -30,7 +30,7 @@
     <maxVersion></maxVersion>
     <jdkPreference>jdkOnly</jdkPreference>
     <runtimeBits>64</runtimeBits>
-    <opt>-Disabelle.root=&quot;%EXEDIR%&quot; -Dcygwin.root=&quot;%EXEDIR%\contrib\cygwin&quot;</opt>
+    <opt>-Disabelle.root=&quot;%EXEDIR%&quot; -Djava.ext.dirs=&quot;%EXEDIR%\contrib\jdk\x86_64-windows\jre\lib\ext&quot; -Dcygwin.root=&quot;%EXEDIR%\contrib\cygwin&quot;</opt>
   </jre>
   <splash>
     <file>{SPLASH}</file>
diff -r f1ba59ddd9a6 -r b8e093f7a802 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Tue Jan 23 12:28:46 2018 +0100
+++ b/Admin/components/components.sha1	Tue Jan 23 20:43:18 2018 +0100
@@ -87,6 +87,7 @@
 51531a3a0c16e180ed95cb7d2bd680c2ec0aa553  jdk-8u131.tar.gz
 e45edcf184f608d6f4a7b966d65a5d3289462693  jdk-8u144.tar.gz
 264e806b9300a4fb3b6e15ba0e2c664d4ea698c8  jdk-8u152.tar.gz
+84b04d877a2ea3a4e2082297b540e14f76722bc5  jdk-8u162.tar.gz
 cfecb1383faaf027ffbabfcd77a0b6a6521e0969  jdk-8u20.tar.gz
 44ffeeae219782d40ce6822b580e608e72fd4c76  jdk-8u31.tar.gz
 4132cf52d5025bf330d53b96a5c6466fef432377  jdk-8u51.tar.gz
diff -r f1ba59ddd9a6 -r b8e093f7a802 Admin/components/main
--- a/Admin/components/main	Tue Jan 23 12:28:46 2018 +0100
+++ b/Admin/components/main	Tue Jan 23 20:43:18 2018 +0100
@@ -5,7 +5,7 @@
 cvc4-1.5-3
 e-2.0-1
 isabelle_fonts-20180113
-jdk-8u152
+jdk-8u162
 jedit_build-20170319
 jfreechart-1.0.14-1
 jortho-1.0-2
diff -r f1ba59ddd9a6 -r b8e093f7a802 bin/isabelle_java
--- a/bin/isabelle_java	Tue Jan 23 12:28:46 2018 +0100
+++ b/bin/isabelle_java	Tue Jan 23 20:43:18 2018 +0100
@@ -66,6 +66,8 @@
   else
     unset ISABELLE_HOME
     unset CLASSPATH
-    exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" -classpath "$ISABELLE_CLASSPATH" "$@"
+    exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" \
+      "-Djava.ext.dirs=$JAVA_HOME/lib/ext" \
+      -classpath "$ISABELLE_CLASSPATH" "$@"
   fi
 }
diff -r f1ba59ddd9a6 -r b8e093f7a802 lib/Tools/java
--- a/lib/Tools/java	Tue Jan 23 12:28:46 2018 +0100
+++ b/lib/Tools/java	Tue Jan 23 20:43:18 2018 +0100
@@ -10,4 +10,5 @@
 unset CLASSPATH
 
 isabelle_java java "${JAVA_ARGS[@]}" \
+  "-Djava.ext.dirs=$(platform_path "$ISABELLE_JDK_HOME/jre/lib/ext")" \
   -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff -r f1ba59ddd9a6 -r b8e093f7a802 lib/Tools/scala
--- a/lib/Tools/scala	Tue Jan 23 12:28:46 2018 +0100
+++ b/lib/Tools/scala	Tue Jan 23 20:43:18 2018 +0100
@@ -14,4 +14,5 @@
 done
 
 isabelle_scala scala "${SCALA_ARGS[@]}" \
+  "-Djava.ext.dirs=$(platform_path "$ISABELLE_JDK_HOME/jre/lib/ext")" \
   -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff -r f1ba59ddd9a6 -r b8e093f7a802 lib/Tools/scalac
--- a/lib/Tools/scalac	Tue Jan 23 12:28:46 2018 +0100
+++ b/lib/Tools/scalac	Tue Jan 23 20:43:18 2018 +0100
@@ -7,5 +7,5 @@
 isabelle_admin_build jars || exit $?
 
 isabelle_scala scalac -Dfile.encoding=UTF-8 \
+  "-Djava.ext.dirs=$(platform_path "$ISABELLE_JDK_HOME/jre/lib/ext")" \
   -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
-
diff -r f1ba59ddd9a6 -r b8e093f7a802 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Jan 23 12:28:46 2018 +0100
+++ b/src/Pure/ML/ml_process.scala	Tue Jan 23 20:43:18 2018 +0100
@@ -101,8 +101,12 @@
                 ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
           def print_list(list: List[String]): String =
             ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
+          def print_sessions(list: List[(String, Position.T)]): String =
+            ML_Syntax.print_list(
+              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
+
           List("Resources.init_session_base" +
-            " {sessions = " + print_list(base.known.sessions.toList) +
+            " {sessions = " + print_sessions(base.known.sessions.toList) +
             ", doc_names = " + print_list(base.doc_names) +
             ", global_theories = " + print_table(base.global_theories.toList) +
             ", loaded_theories = " + print_list(base.loaded_theories.keys) +
diff -r f1ba59ddd9a6 -r b8e093f7a802 src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala	Tue Jan 23 12:28:46 2018 +0100
+++ b/src/Pure/ML/ml_syntax.scala	Tue Jan 23 20:43:18 2018 +0100
@@ -56,4 +56,10 @@
 
   def print_list[A](f: A => String)(list: List[A]): String =
     "[" + commas(list.map(f)) + "]"
+
+
+  /* properties */
+
+  def print_properties(props: Properties.T): String =
+    print_list(print_pair(print_string_bytes(_), print_string_bytes(_))(_))(props)
 }
diff -r f1ba59ddd9a6 -r b8e093f7a802 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Tue Jan 23 12:28:46 2018 +0100
+++ b/src/Pure/PIDE/protocol.ML	Tue Jan 23 20:43:18 2018 +0100
@@ -24,10 +24,12 @@
       let
         val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
         val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
+        val decode_sessions =
+          YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
       in
         Resources.init_session_base
-          {sessions = decode_list sessions_yxml,
-           doc_names = decode_list doc_names_yxml,
+          {sessions = decode_sessions sessions_yxml,
+           docs = decode_list doc_names_yxml,
            global_theories = decode_table global_theories_yxml,
            loaded_theories = decode_list loaded_theories_yxml,
            known_theories = decode_table known_theories_yxml}
diff -r f1ba59ddd9a6 -r b8e093f7a802 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Jan 23 12:28:46 2018 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Jan 23 20:43:18 2018 +0100
@@ -338,11 +338,17 @@
     Symbol.encode_yxml(list(string)(lst))
   }
 
+  private def encode_sessions(lst: List[(String, Position.T)]): String =
+  {
+    import XML.Encode._
+    Symbol.encode_yxml(list(pair(string, properties))(lst))
+  }
+
   def session_base(resources: Resources)
   {
     val base = resources.session_base.standard_path
     protocol_command("Prover.init_session_base",
-      encode_list(base.known.sessions.toList),
+      encode_sessions(base.known.sessions.toList),
       encode_list(base.doc_names),
       encode_table(base.global_theories.toList),
       encode_list(base.loaded_theories.keys),
diff -r f1ba59ddd9a6 -r b8e093f7a802 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Tue Jan 23 12:28:46 2018 +0100
+++ b/src/Pure/PIDE/resources.ML	Tue Jan 23 20:43:18 2018 +0100
@@ -8,8 +8,8 @@
 sig
   val default_qualifier: string
   val init_session_base:
-    {sessions: string list,
-     doc_names: string list,
+    {sessions: (string * Properties.T) list,
+     docs: string list,
      global_theories: (string * string) list,
      loaded_theories: string list,
      known_theories: (string * string) list} -> unit
@@ -45,9 +45,14 @@
 
 val default_qualifier = "Draft";
 
+type entry = {pos: Position.T, serial: serial};
+
+fun make_entry props : entry =
+  {pos = Position.of_properties props, serial = serial ()};
+
 val empty_session_base =
-  {sessions = []: string list,
-   doc_names = []: string list,
+  {sessions = []: (string * entry) list,
+   docs = []: (string * entry) list,
    global_theories = Symtab.empty: string Symtab.table,
    loaded_theories = Symtab.empty: unit Symtab.table,
    known_theories = Symtab.empty: Path.T Symtab.table};
@@ -55,11 +60,11 @@
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
 
-fun init_session_base {sessions, doc_names, global_theories, loaded_theories, known_theories} =
+fun init_session_base {sessions, docs, global_theories, loaded_theories, known_theories} =
   Synchronized.change global_session_base
     (fn _ =>
-      {sessions = sort_strings sessions,
-       doc_names = doc_names,
+      {sessions = sort_by #1 (map (apsnd make_entry) sessions),
+       docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
        global_theories = Symtab.make global_theories,
        loaded_theories = Symtab.make_set loaded_theories,
        known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
@@ -68,7 +73,7 @@
   Synchronized.change global_session_base
     (fn {global_theories, loaded_theories, ...} =>
       {sessions = [],
-       doc_names = [],
+       docs = [],
        global_theories = global_theories,
        loaded_theories = loaded_theories,
        known_theories = #known_theories empty_session_base});
@@ -80,23 +85,28 @@
 fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
 
 fun check_name which kind markup ctxt (name, pos) =
-  let val names = get_session_base which in
-    if member (op =) names name then
-      (Context_Position.report ctxt pos (markup name); name)
-    else
-      let
-        val completion =
-          Completion.make (name, pos) (fn completed =>
-              names
-              |> filter completed
-              |> sort_strings
-              |> map (fn a => (a, (kind, a))));
-        val report = Markup.markup_report (Completion.reported_text completion);
-      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end
+  let val entries = get_session_base which in
+    (case AList.lookup (op =) entries name of
+      SOME entry => (Context_Position.report ctxt pos (markup name entry); name)
+    | NONE =>
+        let
+          val completion =
+            Completion.make (name, pos) (fn completed =>
+                entries
+                |> map #1
+                |> filter completed
+                |> sort_strings
+                |> map (fn a => (a, (kind, a))));
+          val report = Markup.markup_report (Completion.reported_text completion);
+        in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end)
   end;
 
-val check_session = check_name #sessions "session" (Markup.entity Markup.sessionN);
-val check_doc = check_name #doc_names "documentation" Markup.doc;
+fun markup_session name {pos, serial} =
+  Markup.properties
+    (Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name);
+
+val check_session = check_name #sessions "session" markup_session;
+val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name);
 
 
 
diff -r f1ba59ddd9a6 -r b8e093f7a802 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Jan 23 12:28:46 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Jan 23 20:43:18 2018 +0100
@@ -40,7 +40,7 @@
     val empty: Known = Known()
 
     def make(local_dir: Path, bases: List[Base],
-      sessions: List[String] = Nil,
+      sessions: List[(String, Position.T)] = Nil,
       theories: List[Document.Node.Name] = Nil,
       loaded_files: List[(String, List[Path])] = Nil): Known =
     {
@@ -57,7 +57,7 @@
       }
 
       val known_sessions =
-        (sessions.toSet /: bases)({ case (known, base) => known ++ base.known.sessions })
+        (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
 
       val known_theories =
         (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
@@ -96,7 +96,7 @@
   }
 
   sealed case class Known(
-    sessions: Set[String] = Set.empty,
+    sessions: Map[String, Position.T] = Map.empty,
     theories: Map[String, Document.Node.Name] = Map.empty,
     theories_local: Map[String, Document.Node.Name] = Map.empty,
     files: Map[JFile, List[Document.Node.Name]] = Map.empty,
@@ -317,7 +317,7 @@
 
             val known =
               Known.make(info.dir, List(imports_base),
-                sessions = List(info.name),
+                sessions = List(info.name -> info.pos),
                 theories = dependencies.theories,
                 loaded_files = loaded_files)
 
diff -r f1ba59ddd9a6 -r b8e093f7a802 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Jan 23 12:28:46 2018 +0100
+++ b/src/Pure/Tools/build.ML	Tue Jan 23 20:43:18 2018 +0100
@@ -149,7 +149,7 @@
   name: string,
   master_dir: Path.T,
   theories: (Options.T * (string * Position.T) list) list,
-  sessions: string list,
+  sessions: (string * Properties.T) list,
   doc_names: string list,
   global_theories: (string * string) list,
   loaded_theories: string list,
@@ -168,8 +168,9 @@
         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
           (pair string
             (pair (((list (pair Options.decode (list (pair string position))))))
-              (pair (list string) (pair (list string) (pair (list (pair string string)) (pair (list string)
-                (pair (list (pair string string)) (list string)))))))))))))))))
+              (pair (list (pair string properties)) (pair (list string)
+                (pair (list (pair string string)) (pair (list string)
+                  (pair (list (pair string string)) (list string)))))))))))))))))
       (YXML.parse_body yxml);
   in
     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
@@ -190,7 +191,7 @@
     val _ =
       Resources.init_session_base
         {sessions = sessions,
-         doc_names = doc_names,
+         docs = doc_names,
          global_theories = global_theories,
          loaded_theories = loaded_theories,
          known_theories = known_theories};
diff -r f1ba59ddd9a6 -r b8e093f7a802 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Jan 23 12:28:46 2018 +0100
+++ b/src/Pure/Tools/build.scala	Tue Jan 23 20:43:18 2018 +0100
@@ -212,7 +212,8 @@
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
                 pair(list(pair(Options.encode, list(pair(string, properties)))),
-                pair(list(string), pair(list(string), pair(list(pair(string, string)),
+                pair(list(pair(string, properties)), pair(list(string),
+                pair(list(pair(string, string)),
                 pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),