merged
authorwenzelm
Tue Jan 23 20:43:18 2018 +0100 (22 months ago ago)
changeset 67494b8e093f7a802
parent 67489 f1ba59ddd9a6
parent 67493 c4e9e0c50487
child 67495 90d760fa8f34
merged
     1.1 --- a/Admin/Linux/Isabelle.run	Tue Jan 23 12:28:46 2018 +0100
     1.2 +++ b/Admin/Linux/Isabelle.run	Tue Jan 23 20:43:18 2018 +0100
     1.3 @@ -20,11 +20,7 @@
     1.4  # Java runtime options
     1.5  
     1.6  ISABELLE_NAME="$(basename "$0" .run)"
     1.7 -if [ -z "$ISABELLE_PLATFORM64" ]; then
     1.8 -  declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options32"))
     1.9 -else
    1.10 -  declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options64"))
    1.11 -fi
    1.12 +declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options"))
    1.13  
    1.14  
    1.15  # main
    1.16 @@ -32,8 +28,9 @@
    1.17  #paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
    1.18  unset XMODIFIERS
    1.19  
    1.20 -exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/jre/bin/java" \
    1.21 +exec "$ISABELLE_HOME/contrib/jdk/x86_64-linux/jre/bin/java" \
    1.22    "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
    1.23 +  "-Djava.ext.dirs=$ISABELLE_HOME/contrib/jdk/x86_64-linux/jre/lib/ext" \
    1.24    -classpath "{CLASSPATH}" \
    1.25    "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
    1.26    isabelle.Main "$@"
     2.1 --- a/Admin/MacOS/Info.plist-part2	Tue Jan 23 12:28:46 2018 +0100
     2.2 +++ b/Admin/MacOS/Info.plist-part2	Tue Jan 23 20:43:18 2018 +0100
     2.3 @@ -1,4 +1,5 @@
     2.4  <string>-Disabelle.root=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string>
     2.5 +<string>-Djava.ext.dirs=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}/contrib/jdk/x86_64-darwin/Contents/Home/jre/lib/ext</string>
     2.6  <string>-Disabelle.app=true</string>
     2.7  </array>
     2.8  <key>JVMArguments</key>
     3.1 --- a/Admin/Windows/launch4j/isabelle.xml	Tue Jan 23 12:28:46 2018 +0100
     3.2 +++ b/Admin/Windows/launch4j/isabelle.xml	Tue Jan 23 20:43:18 2018 +0100
     3.3 @@ -30,7 +30,7 @@
     3.4      <maxVersion></maxVersion>
     3.5      <jdkPreference>jdkOnly</jdkPreference>
     3.6      <runtimeBits>64</runtimeBits>
     3.7 -    <opt>-Disabelle.root=&quot;%EXEDIR%&quot; -Dcygwin.root=&quot;%EXEDIR%\contrib\cygwin&quot;</opt>
     3.8 +    <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>
     3.9    </jre>
    3.10    <splash>
    3.11      <file>{SPLASH}</file>
     4.1 --- a/Admin/components/components.sha1	Tue Jan 23 12:28:46 2018 +0100
     4.2 +++ b/Admin/components/components.sha1	Tue Jan 23 20:43:18 2018 +0100
     4.3 @@ -87,6 +87,7 @@
     4.4  51531a3a0c16e180ed95cb7d2bd680c2ec0aa553  jdk-8u131.tar.gz
     4.5  e45edcf184f608d6f4a7b966d65a5d3289462693  jdk-8u144.tar.gz
     4.6  264e806b9300a4fb3b6e15ba0e2c664d4ea698c8  jdk-8u152.tar.gz
     4.7 +84b04d877a2ea3a4e2082297b540e14f76722bc5  jdk-8u162.tar.gz
     4.8  cfecb1383faaf027ffbabfcd77a0b6a6521e0969  jdk-8u20.tar.gz
     4.9  44ffeeae219782d40ce6822b580e608e72fd4c76  jdk-8u31.tar.gz
    4.10  4132cf52d5025bf330d53b96a5c6466fef432377  jdk-8u51.tar.gz
     5.1 --- a/Admin/components/main	Tue Jan 23 12:28:46 2018 +0100
     5.2 +++ b/Admin/components/main	Tue Jan 23 20:43:18 2018 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  cvc4-1.5-3
     5.5  e-2.0-1
     5.6  isabelle_fonts-20180113
     5.7 -jdk-8u152
     5.8 +jdk-8u162
     5.9  jedit_build-20170319
    5.10  jfreechart-1.0.14-1
    5.11  jortho-1.0-2
     6.1 --- a/bin/isabelle_java	Tue Jan 23 12:28:46 2018 +0100
     6.2 +++ b/bin/isabelle_java	Tue Jan 23 20:43:18 2018 +0100
     6.3 @@ -66,6 +66,8 @@
     6.4    else
     6.5      unset ISABELLE_HOME
     6.6      unset CLASSPATH
     6.7 -    exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" -classpath "$ISABELLE_CLASSPATH" "$@"
     6.8 +    exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" \
     6.9 +      "-Djava.ext.dirs=$JAVA_HOME/lib/ext" \
    6.10 +      -classpath "$ISABELLE_CLASSPATH" "$@"
    6.11    fi
    6.12  }
     7.1 --- a/lib/Tools/java	Tue Jan 23 12:28:46 2018 +0100
     7.2 +++ b/lib/Tools/java	Tue Jan 23 20:43:18 2018 +0100
     7.3 @@ -10,4 +10,5 @@
     7.4  unset CLASSPATH
     7.5  
     7.6  isabelle_java java "${JAVA_ARGS[@]}" \
     7.7 +  "-Djava.ext.dirs=$(platform_path "$ISABELLE_JDK_HOME/jre/lib/ext")" \
     7.8    -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
     8.1 --- a/lib/Tools/scala	Tue Jan 23 12:28:46 2018 +0100
     8.2 +++ b/lib/Tools/scala	Tue Jan 23 20:43:18 2018 +0100
     8.3 @@ -14,4 +14,5 @@
     8.4  done
     8.5  
     8.6  isabelle_scala scala "${SCALA_ARGS[@]}" \
     8.7 +  "-Djava.ext.dirs=$(platform_path "$ISABELLE_JDK_HOME/jre/lib/ext")" \
     8.8    -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
     9.1 --- a/lib/Tools/scalac	Tue Jan 23 12:28:46 2018 +0100
     9.2 +++ b/lib/Tools/scalac	Tue Jan 23 20:43:18 2018 +0100
     9.3 @@ -7,5 +7,5 @@
     9.4  isabelle_admin_build jars || exit $?
     9.5  
     9.6  isabelle_scala scalac -Dfile.encoding=UTF-8 \
     9.7 +  "-Djava.ext.dirs=$(platform_path "$ISABELLE_JDK_HOME/jre/lib/ext")" \
     9.8    -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
     9.9 -
    10.1 --- a/src/Pure/ML/ml_process.scala	Tue Jan 23 12:28:46 2018 +0100
    10.2 +++ b/src/Pure/ML/ml_process.scala	Tue Jan 23 20:43:18 2018 +0100
    10.3 @@ -101,8 +101,12 @@
    10.4                  ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
    10.5            def print_list(list: List[String]): String =
    10.6              ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
    10.7 +          def print_sessions(list: List[(String, Position.T)]): String =
    10.8 +            ML_Syntax.print_list(
    10.9 +              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
   10.10 +
   10.11            List("Resources.init_session_base" +
   10.12 -            " {sessions = " + print_list(base.known.sessions.toList) +
   10.13 +            " {sessions = " + print_sessions(base.known.sessions.toList) +
   10.14              ", doc_names = " + print_list(base.doc_names) +
   10.15              ", global_theories = " + print_table(base.global_theories.toList) +
   10.16              ", loaded_theories = " + print_list(base.loaded_theories.keys) +
    11.1 --- a/src/Pure/ML/ml_syntax.scala	Tue Jan 23 12:28:46 2018 +0100
    11.2 +++ b/src/Pure/ML/ml_syntax.scala	Tue Jan 23 20:43:18 2018 +0100
    11.3 @@ -56,4 +56,10 @@
    11.4  
    11.5    def print_list[A](f: A => String)(list: List[A]): String =
    11.6      "[" + commas(list.map(f)) + "]"
    11.7 +
    11.8 +
    11.9 +  /* properties */
   11.10 +
   11.11 +  def print_properties(props: Properties.T): String =
   11.12 +    print_list(print_pair(print_string_bytes(_), print_string_bytes(_))(_))(props)
   11.13  }
    12.1 --- a/src/Pure/PIDE/protocol.ML	Tue Jan 23 12:28:46 2018 +0100
    12.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Jan 23 20:43:18 2018 +0100
    12.3 @@ -24,10 +24,12 @@
    12.4        let
    12.5          val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
    12.6          val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
    12.7 +        val decode_sessions =
    12.8 +          YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
    12.9        in
   12.10          Resources.init_session_base
   12.11 -          {sessions = decode_list sessions_yxml,
   12.12 -           doc_names = decode_list doc_names_yxml,
   12.13 +          {sessions = decode_sessions sessions_yxml,
   12.14 +           docs = decode_list doc_names_yxml,
   12.15             global_theories = decode_table global_theories_yxml,
   12.16             loaded_theories = decode_list loaded_theories_yxml,
   12.17             known_theories = decode_table known_theories_yxml}
    13.1 --- a/src/Pure/PIDE/protocol.scala	Tue Jan 23 12:28:46 2018 +0100
    13.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Jan 23 20:43:18 2018 +0100
    13.3 @@ -338,11 +338,17 @@
    13.4      Symbol.encode_yxml(list(string)(lst))
    13.5    }
    13.6  
    13.7 +  private def encode_sessions(lst: List[(String, Position.T)]): String =
    13.8 +  {
    13.9 +    import XML.Encode._
   13.10 +    Symbol.encode_yxml(list(pair(string, properties))(lst))
   13.11 +  }
   13.12 +
   13.13    def session_base(resources: Resources)
   13.14    {
   13.15      val base = resources.session_base.standard_path
   13.16      protocol_command("Prover.init_session_base",
   13.17 -      encode_list(base.known.sessions.toList),
   13.18 +      encode_sessions(base.known.sessions.toList),
   13.19        encode_list(base.doc_names),
   13.20        encode_table(base.global_theories.toList),
   13.21        encode_list(base.loaded_theories.keys),
    14.1 --- a/src/Pure/PIDE/resources.ML	Tue Jan 23 12:28:46 2018 +0100
    14.2 +++ b/src/Pure/PIDE/resources.ML	Tue Jan 23 20:43:18 2018 +0100
    14.3 @@ -8,8 +8,8 @@
    14.4  sig
    14.5    val default_qualifier: string
    14.6    val init_session_base:
    14.7 -    {sessions: string list,
    14.8 -     doc_names: string list,
    14.9 +    {sessions: (string * Properties.T) list,
   14.10 +     docs: string list,
   14.11       global_theories: (string * string) list,
   14.12       loaded_theories: string list,
   14.13       known_theories: (string * string) list} -> unit
   14.14 @@ -45,9 +45,14 @@
   14.15  
   14.16  val default_qualifier = "Draft";
   14.17  
   14.18 +type entry = {pos: Position.T, serial: serial};
   14.19 +
   14.20 +fun make_entry props : entry =
   14.21 +  {pos = Position.of_properties props, serial = serial ()};
   14.22 +
   14.23  val empty_session_base =
   14.24 -  {sessions = []: string list,
   14.25 -   doc_names = []: string list,
   14.26 +  {sessions = []: (string * entry) list,
   14.27 +   docs = []: (string * entry) list,
   14.28     global_theories = Symtab.empty: string Symtab.table,
   14.29     loaded_theories = Symtab.empty: unit Symtab.table,
   14.30     known_theories = Symtab.empty: Path.T Symtab.table};
   14.31 @@ -55,11 +60,11 @@
   14.32  val global_session_base =
   14.33    Synchronized.var "Sessions.base" empty_session_base;
   14.34  
   14.35 -fun init_session_base {sessions, doc_names, global_theories, loaded_theories, known_theories} =
   14.36 +fun init_session_base {sessions, docs, global_theories, loaded_theories, known_theories} =
   14.37    Synchronized.change global_session_base
   14.38      (fn _ =>
   14.39 -      {sessions = sort_strings sessions,
   14.40 -       doc_names = doc_names,
   14.41 +      {sessions = sort_by #1 (map (apsnd make_entry) sessions),
   14.42 +       docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
   14.43         global_theories = Symtab.make global_theories,
   14.44         loaded_theories = Symtab.make_set loaded_theories,
   14.45         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
   14.46 @@ -68,7 +73,7 @@
   14.47    Synchronized.change global_session_base
   14.48      (fn {global_theories, loaded_theories, ...} =>
   14.49        {sessions = [],
   14.50 -       doc_names = [],
   14.51 +       docs = [],
   14.52         global_theories = global_theories,
   14.53         loaded_theories = loaded_theories,
   14.54         known_theories = #known_theories empty_session_base});
   14.55 @@ -80,23 +85,28 @@
   14.56  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
   14.57  
   14.58  fun check_name which kind markup ctxt (name, pos) =
   14.59 -  let val names = get_session_base which in
   14.60 -    if member (op =) names name then
   14.61 -      (Context_Position.report ctxt pos (markup name); name)
   14.62 -    else
   14.63 -      let
   14.64 -        val completion =
   14.65 -          Completion.make (name, pos) (fn completed =>
   14.66 -              names
   14.67 -              |> filter completed
   14.68 -              |> sort_strings
   14.69 -              |> map (fn a => (a, (kind, a))));
   14.70 -        val report = Markup.markup_report (Completion.reported_text completion);
   14.71 -      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end
   14.72 +  let val entries = get_session_base which in
   14.73 +    (case AList.lookup (op =) entries name of
   14.74 +      SOME entry => (Context_Position.report ctxt pos (markup name entry); name)
   14.75 +    | NONE =>
   14.76 +        let
   14.77 +          val completion =
   14.78 +            Completion.make (name, pos) (fn completed =>
   14.79 +                entries
   14.80 +                |> map #1
   14.81 +                |> filter completed
   14.82 +                |> sort_strings
   14.83 +                |> map (fn a => (a, (kind, a))));
   14.84 +          val report = Markup.markup_report (Completion.reported_text completion);
   14.85 +        in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end)
   14.86    end;
   14.87  
   14.88 -val check_session = check_name #sessions "session" (Markup.entity Markup.sessionN);
   14.89 -val check_doc = check_name #doc_names "documentation" Markup.doc;
   14.90 +fun markup_session name {pos, serial} =
   14.91 +  Markup.properties
   14.92 +    (Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name);
   14.93 +
   14.94 +val check_session = check_name #sessions "session" markup_session;
   14.95 +val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name);
   14.96  
   14.97  
   14.98  
    15.1 --- a/src/Pure/Thy/sessions.scala	Tue Jan 23 12:28:46 2018 +0100
    15.2 +++ b/src/Pure/Thy/sessions.scala	Tue Jan 23 20:43:18 2018 +0100
    15.3 @@ -40,7 +40,7 @@
    15.4      val empty: Known = Known()
    15.5  
    15.6      def make(local_dir: Path, bases: List[Base],
    15.7 -      sessions: List[String] = Nil,
    15.8 +      sessions: List[(String, Position.T)] = Nil,
    15.9        theories: List[Document.Node.Name] = Nil,
   15.10        loaded_files: List[(String, List[Path])] = Nil): Known =
   15.11      {
   15.12 @@ -57,7 +57,7 @@
   15.13        }
   15.14  
   15.15        val known_sessions =
   15.16 -        (sessions.toSet /: bases)({ case (known, base) => known ++ base.known.sessions })
   15.17 +        (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
   15.18  
   15.19        val known_theories =
   15.20          (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
   15.21 @@ -96,7 +96,7 @@
   15.22    }
   15.23  
   15.24    sealed case class Known(
   15.25 -    sessions: Set[String] = Set.empty,
   15.26 +    sessions: Map[String, Position.T] = Map.empty,
   15.27      theories: Map[String, Document.Node.Name] = Map.empty,
   15.28      theories_local: Map[String, Document.Node.Name] = Map.empty,
   15.29      files: Map[JFile, List[Document.Node.Name]] = Map.empty,
   15.30 @@ -317,7 +317,7 @@
   15.31  
   15.32              val known =
   15.33                Known.make(info.dir, List(imports_base),
   15.34 -                sessions = List(info.name),
   15.35 +                sessions = List(info.name -> info.pos),
   15.36                  theories = dependencies.theories,
   15.37                  loaded_files = loaded_files)
   15.38  
    16.1 --- a/src/Pure/Tools/build.ML	Tue Jan 23 12:28:46 2018 +0100
    16.2 +++ b/src/Pure/Tools/build.ML	Tue Jan 23 20:43:18 2018 +0100
    16.3 @@ -149,7 +149,7 @@
    16.4    name: string,
    16.5    master_dir: Path.T,
    16.6    theories: (Options.T * (string * Position.T) list) list,
    16.7 -  sessions: string list,
    16.8 +  sessions: (string * Properties.T) list,
    16.9    doc_names: string list,
   16.10    global_theories: (string * string) list,
   16.11    loaded_theories: string list,
   16.12 @@ -168,8 +168,9 @@
   16.13          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
   16.14            (pair string
   16.15              (pair (((list (pair Options.decode (list (pair string position))))))
   16.16 -              (pair (list string) (pair (list string) (pair (list (pair string string)) (pair (list string)
   16.17 -                (pair (list (pair string string)) (list string)))))))))))))))))
   16.18 +              (pair (list (pair string properties)) (pair (list string)
   16.19 +                (pair (list (pair string string)) (pair (list string)
   16.20 +                  (pair (list (pair string string)) (list string)))))))))))))))))
   16.21        (YXML.parse_body yxml);
   16.22    in
   16.23      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
   16.24 @@ -190,7 +191,7 @@
   16.25      val _ =
   16.26        Resources.init_session_base
   16.27          {sessions = sessions,
   16.28 -         doc_names = doc_names,
   16.29 +         docs = doc_names,
   16.30           global_theories = global_theories,
   16.31           loaded_theories = loaded_theories,
   16.32           known_theories = known_theories};
    17.1 --- a/src/Pure/Tools/build.scala	Tue Jan 23 12:28:46 2018 +0100
    17.2 +++ b/src/Pure/Tools/build.scala	Tue Jan 23 20:43:18 2018 +0100
    17.3 @@ -212,7 +212,8 @@
    17.4                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    17.5                  pair(string, pair(string, pair(string, pair(Path.encode,
    17.6                  pair(list(pair(Options.encode, list(pair(string, properties)))),
    17.7 -                pair(list(string), pair(list(string), pair(list(pair(string, string)),
    17.8 +                pair(list(pair(string, properties)), pair(list(string),
    17.9 +                pair(list(pair(string, string)),
   17.10                  pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
   17.11                (Symbol.codes, (command_timings, (do_output, (verbose,
   17.12                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),