merged
authorwenzelm
Fri Apr 21 20:36:20 2017 +0200 (2017-04-21)
changeset 65544c09c11386ca5
parent 65516 03efd17e083b
parent 65543 8369b33fda0a
child 65545 42c4b87e98c2
merged
NEWS
src/HOL/ROOT
     1.1 --- a/NEWS	Thu Apr 20 16:21:29 2017 +0200
     1.2 +++ b/NEWS	Fri Apr 21 20:36:20 2017 +0200
     1.3 @@ -56,9 +56,6 @@
     1.4  entry of the specified logic session in the editor, while its parent is
     1.5  used for formal checking.
     1.6  
     1.7 -* Improved support for editing of a complex session hierarchy with
     1.8 -session-qualified theory imports: "isabelle jedit -A".
     1.9 -
    1.10  * The PIDE document model maintains file content independently of the
    1.11  status of jEdit editor buffers. Reloading jEdit buffers no longer causes
    1.12  changes of formal document content. Theory dependencies are always
     2.1 --- a/etc/settings	Thu Apr 20 16:21:29 2017 +0200
     2.2 +++ b/etc/settings	Fri Apr 21 20:36:20 2017 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  ### Isabelle/Scala
     2.5  ###
     2.6  
     2.7 -ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130"
     2.8 +ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms128m -J-Xmx1024m -J-Xss2m"
     2.9  
    2.10  ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0"
    2.11  
     3.1 --- a/src/Doc/JEdit/JEdit.thy	Thu Apr 20 16:21:29 2017 +0200
     3.2 +++ b/src/Doc/JEdit/JEdit.thy	Fri Apr 21 20:36:20 2017 +0200
     3.3 @@ -231,7 +231,6 @@
     3.4  \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
     3.5  
     3.6    Options are:
     3.7 -    -A           explore theory imports of all known sessions
     3.8      -D NAME=X    set JVM system property
     3.9      -J OPTION    add JVM runtime option
    3.10      -R           open ROOT entry of logic session and use its parent
    3.11 @@ -258,11 +257,6 @@
    3.12    The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
    3.13    session image.
    3.14  
    3.15 -  Option \<^verbatim>\<open>-A\<close> explores theory imports of all known sessions (according to the
    3.16 -  directories specified via option \<^verbatim>\<open>-d\<close>). This facilitates editing of a
    3.17 -  complex session hierarchy with session-qualified theory imports, while using
    3.18 -  a different base session image than usual.
    3.19 -
    3.20    Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close> as follows: the \<^verbatim>\<open>ROOT\<close>
    3.21    entry of the specified session is opened in the editor, while its parent
    3.22    session is used for formal checking. This facilitates maintenance of a
     4.1 --- a/src/FOLP/ROOT	Thu Apr 20 16:21:29 2017 +0200
     4.2 +++ b/src/FOLP/ROOT	Fri Apr 21 20:36:20 2017 +0200
     4.3 @@ -10,7 +10,9 @@
     4.4      Presence of unknown proof term means that matching does not behave as expected.
     4.5    *}
     4.6    options [document = false]
     4.7 -  theories FOLP
     4.8 +  theories
     4.9 +    IFOLP (global)
    4.10 +    FOLP (global)
    4.11  
    4.12  session "FOLP-ex" in ex = FOLP +
    4.13    description {*
     5.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Thu Apr 20 16:21:29 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Fri Apr 21 20:36:20 2017 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4  text\<open>Also Cauchy's residue theorem by Wenda Li (2016)\<close>
     5.5  
     5.6  theory Conformal_Mappings
     5.7 -imports "Cauchy_Integral_Theorem"
     5.8 +imports Cauchy_Integral_Theorem
     5.9  
    5.10  begin
    5.11  
     6.1 --- a/src/HOL/Auth/Auth_Public.thy	Thu Apr 20 16:21:29 2017 +0200
     6.2 +++ b/src/HOL/Auth/Auth_Public.thy	Fri Apr 21 20:36:20 2017 +0200
     6.3 @@ -6,10 +6,10 @@
     6.4  
     6.5  theory Auth_Public
     6.6  imports
     6.7 -  "NS_Public_Bad"
     6.8 -  "NS_Public"
     6.9 -  "TLS"
    6.10 -  "CertifiedEmail"
    6.11 +  NS_Public_Bad
    6.12 +  NS_Public
    6.13 +  TLS
    6.14 +  CertifiedEmail
    6.15  begin
    6.16  
    6.17  end
     7.1 --- a/src/HOL/Auth/Auth_Shared.thy	Thu Apr 20 16:21:29 2017 +0200
     7.2 +++ b/src/HOL/Auth/Auth_Shared.thy	Fri Apr 21 20:36:20 2017 +0200
     7.3 @@ -6,22 +6,22 @@
     7.4  
     7.5  theory Auth_Shared
     7.6  imports
     7.7 -  "NS_Shared"
     7.8 -  "Kerberos_BAN"
     7.9 -  "Kerberos_BAN_Gets"
    7.10 -  "KerberosIV"
    7.11 -  "KerberosIV_Gets"
    7.12 -  "KerberosV"
    7.13 -  "OtwayRees"
    7.14 -  "OtwayRees_AN"
    7.15 -  "OtwayRees_Bad"
    7.16 -  "OtwayReesBella"
    7.17 -  "WooLam"
    7.18 -  "Recur"
    7.19 -  "Yahalom"
    7.20 -  "Yahalom2"
    7.21 -  "Yahalom_Bad"
    7.22 -  "ZhouGollmann"
    7.23 +  NS_Shared
    7.24 +  Kerberos_BAN
    7.25 +  Kerberos_BAN_Gets
    7.26 +  KerberosIV
    7.27 +  KerberosIV_Gets
    7.28 +  KerberosV
    7.29 +  OtwayRees
    7.30 +  OtwayRees_AN
    7.31 +  OtwayRees_Bad
    7.32 +  OtwayReesBella
    7.33 +  WooLam
    7.34 +  Recur
    7.35 +  Yahalom
    7.36 +  Yahalom2
    7.37 +  Yahalom_Bad
    7.38 +  ZhouGollmann
    7.39  begin
    7.40  
    7.41  end
     8.1 --- a/src/HOL/Auth/Guard/Auth_Guard_Public.thy	Thu Apr 20 16:21:29 2017 +0200
     8.2 +++ b/src/HOL/Auth/Guard/Auth_Guard_Public.thy	Fri Apr 21 20:36:20 2017 +0200
     8.3 @@ -6,10 +6,10 @@
     8.4  
     8.5  theory Auth_Guard_Public
     8.6  imports
     8.7 -  "P1"
     8.8 -  "P2"
     8.9 -  "Guard_NS_Public"
    8.10 -  "Proto"
    8.11 +  P1
    8.12 +  P2
    8.13 +  Guard_NS_Public
    8.14 +  Proto
    8.15  begin
    8.16  
    8.17  end
     9.1 --- a/src/HOL/Auth/Guard/Auth_Guard_Shared.thy	Thu Apr 20 16:21:29 2017 +0200
     9.2 +++ b/src/HOL/Auth/Guard/Auth_Guard_Shared.thy	Fri Apr 21 20:36:20 2017 +0200
     9.3 @@ -6,8 +6,8 @@
     9.4  
     9.5  theory Auth_Guard_Shared
     9.6  imports
     9.7 -  "Guard_OtwayRees"
     9.8 -  "Guard_Yahalom"
     9.9 +  Guard_OtwayRees
    9.10 +  Guard_Yahalom
    9.11  begin
    9.12  
    9.13  end
    10.1 --- a/src/HOL/Auth/Smartcard/Auth_Smartcard.thy	Thu Apr 20 16:21:29 2017 +0200
    10.2 +++ b/src/HOL/Auth/Smartcard/Auth_Smartcard.thy	Fri Apr 21 20:36:20 2017 +0200
    10.3 @@ -6,8 +6,8 @@
    10.4  
    10.5  theory Auth_Smartcard
    10.6  imports
    10.7 -  "ShoupRubin"
    10.8 -  "ShoupRubinBella"
    10.9 +  ShoupRubin
   10.10 +  ShoupRubinBella
   10.11  begin
   10.12  
   10.13  end
    11.1 --- a/src/HOL/Corec_Examples/Paper_Examples.thy	Thu Apr 20 16:21:29 2017 +0200
    11.2 +++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Fri Apr 21 20:36:20 2017 +0200
    11.3 @@ -9,7 +9,7 @@
    11.4  section \<open>Small Examples from the Paper ``Friends with Benefits''\<close>
    11.5  
    11.6  theory Paper_Examples
    11.7 -imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/FSet" "Complex_Main"
    11.8 +imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/FSet" Complex_Main
    11.9  begin
   11.10  
   11.11  section \<open>Examples from the introduction\<close>
    12.1 --- a/src/HOL/Library/code_test.ML	Thu Apr 20 16:21:29 2017 +0200
    12.2 +++ b/src/HOL/Library/code_test.ML	Fri Apr 21 20:36:20 2017 +0200
    12.3 @@ -551,11 +551,11 @@
    12.4        "}\n"
    12.5  
    12.6      val compile_cmd =
    12.7 -      "\"$SCALA_HOME/bin/scalac\" $ISABELLE_SCALAC_OPTIONS -d " ^ File.bash_path path ^
    12.8 +      "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ File.bash_path path ^
    12.9        " -classpath " ^ File.bash_path path ^ " " ^
   12.10        File.bash_path code_path ^ " " ^ File.bash_path driver_path
   12.11  
   12.12 -    val run_cmd = "\"$SCALA_HOME/bin/scala\" -cp " ^ File.bash_path path ^ " Test"
   12.13 +    val run_cmd = "isabelle_scala scala -cp " ^ File.bash_path path ^ " Test"
   12.14    in
   12.15      {files = [(driver_path, driver)],
   12.16       compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
    13.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Apr 20 16:21:29 2017 +0200
    13.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Fri Apr 21 20:36:20 2017 +0200
    13.3 @@ -5,7 +5,7 @@
    13.4  (* Compiler correctness statement and proof *)
    13.5  
    13.6  theory CorrComp
    13.7 -imports "../J/JTypeSafe" "LemmasComp"
    13.8 +imports "../J/JTypeSafe" LemmasComp
    13.9  begin
   13.10  
   13.11  declare wf_prog_ws_prog [simp add]
    14.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Thu Apr 20 16:21:29 2017 +0200
    14.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Apr 21 20:36:20 2017 +0200
    14.3 @@ -6,8 +6,7 @@
    14.4  section \<open>Weak normalization for simply-typed lambda calculus\<close>
    14.5  
    14.6  theory WeakNorm
    14.7 -imports LambdaType NormalForm "~~/src/HOL/Library/Old_Datatype"
    14.8 -  "~~/src/HOL/Library/Code_Target_Int"
    14.9 +imports LambdaType NormalForm "HOL-Library.Old_Datatype" "HOL-Library.Code_Target_Int"
   14.10  begin
   14.11  
   14.12  text \<open>
    15.1 --- a/src/HOL/ROOT	Thu Apr 20 16:21:29 2017 +0200
    15.2 +++ b/src/HOL/ROOT	Fri Apr 21 20:36:20 2017 +0200
    15.3 @@ -20,8 +20,12 @@
    15.4    *}
    15.5    options [document = false, theory_qualifier = "HOL",
    15.6      quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
    15.7 -  sessions "HOL-Library"
    15.8 -  theories "HOL-Library.Old_Datatype"
    15.9 +  sessions
   15.10 +    "HOL-Library"
   15.11 +  theories
   15.12 +    GCD
   15.13 +    Binomial
   15.14 +    "HOL-Library.Old_Datatype"
   15.15    files
   15.16      "Tools/Quickcheck/Narrowing_Engine.hs"
   15.17      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
   15.18 @@ -59,6 +63,9 @@
   15.19    document_files "root.bib" "root.tex"
   15.20  
   15.21  session "HOL-Analysis" (main timing) in Analysis = HOL +
   15.22 +  sessions
   15.23 +    "HOL-Library"
   15.24 +    "HOL-Computational_Algebra"
   15.25    theories
   15.26      Analysis
   15.27    document_files
   15.28 @@ -70,6 +77,8 @@
   15.29      Circle_Area
   15.30  
   15.31  session "HOL-Computational_Algebra" in "Computational_Algebra" = HOL +
   15.32 +  sessions
   15.33 +    "HOL-Library"
   15.34    theories
   15.35      Computational_Algebra
   15.36      (*conflicting type class instantiations and dependent applications*)
   15.37 @@ -94,7 +103,10 @@
   15.38      subspaces (not only one-dimensional subspaces), can be extended to a
   15.39      continous linearform on the whole vectorspace.
   15.40    *}
   15.41 -  theories Hahn_Banach
   15.42 +  sessions
   15.43 +    "HOL-Library"
   15.44 +  theories
   15.45 +    Hahn_Banach
   15.46    document_files "root.bib" "root.tex"
   15.47  
   15.48  session "HOL-Induct" in Induct = HOL +
   15.49 @@ -114,6 +126,8 @@
   15.50      Exp demonstrates the use of iterated inductive definitions to reason about
   15.51      mutually recursive relations.
   15.52    *}
   15.53 +  sessions
   15.54 +    "HOL-Library"
   15.55    theories [document = false]
   15.56      "~~/src/HOL/Library/Old_Datatype"
   15.57    theories [quick_and_dirty]
   15.58 @@ -190,7 +204,7 @@
   15.59  session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   15.60    options [document_variants = document]
   15.61    theories [document = false]
   15.62 -    "Less_False"
   15.63 +    Less_False
   15.64      "~~/src/HOL/Library/Multiset"
   15.65      "~~/src/HOL/Number_Theory/Fib"
   15.66    theories
   15.67 @@ -215,6 +229,10 @@
   15.68      Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
   15.69      Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   15.70    *}
   15.71 +  sessions
   15.72 +    "HOL-Library"
   15.73 +    "HOL-Algebra"
   15.74 +    "HOL-Computational_Algebra"
   15.75    theories [document = false]
   15.76      "~~/src/HOL/Library/FuncSet"
   15.77      "~~/src/HOL/Library/Multiset"
   15.78 @@ -243,6 +261,9 @@
   15.79  
   15.80  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   15.81    options [document = false, browser_info = false]
   15.82 +  sessions
   15.83 +    "HOL-Computational_Algebra"
   15.84 +    "HOL-Number_Theory"
   15.85    theories
   15.86      Generate
   15.87      Generate_Binary_Nat
   15.88 @@ -303,6 +324,9 @@
   15.89  
   15.90      The Isabelle Algebraic Library.
   15.91    *}
   15.92 +  sessions
   15.93 +    "HOL-Library"
   15.94 +    "HOL-Computational_Algebra"
   15.95    theories [document = false]
   15.96      (* Preliminaries from set and number theory *)
   15.97      "~~/src/HOL/Library/FuncSet"
   15.98 @@ -348,7 +372,7 @@
   15.99    *}
  15.100    theories
  15.101      (*Basic meta-theory*)
  15.102 -    "UNITY_Main"
  15.103 +    UNITY_Main
  15.104  
  15.105      (*Simple examples: no composition*)
  15.106      "Simple/Deadlock"
  15.107 @@ -380,7 +404,7 @@
  15.108      "Comp/Client"
  15.109  
  15.110      (*obsolete*)
  15.111 -    "ELT"
  15.112 +    ELT
  15.113    document_files "root.tex"
  15.114  
  15.115  session "HOL-Unix" in Unix = HOL +
  15.116 @@ -394,6 +418,8 @@
  15.117  
  15.118  session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
  15.119    options [print_mode = "iff,no_brackets"]
  15.120 +  sessions
  15.121 +    "HOL-Library"
  15.122    theories [document = false]
  15.123      "~~/src/HOL/Library/Countable"
  15.124      "~~/src/HOL/Library/Monad_Syntax"
  15.125 @@ -406,7 +432,11 @@
  15.126      Various decision procedures, typically involving reflection.
  15.127    *}
  15.128    options [document = false]
  15.129 -  theories Decision_Procs
  15.130 +  sessions
  15.131 +    "HOL-Library"
  15.132 +    "HOL-Algebra"
  15.133 +  theories
  15.134 +    Decision_Procs
  15.135  
  15.136  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
  15.137    options [document = false]
  15.138 @@ -420,6 +450,9 @@
  15.139      Examples for program extraction in Higher-Order Logic.
  15.140    *}
  15.141    options [parallel_proofs = 0, quick_and_dirty = false]
  15.142 +  sessions
  15.143 +    "HOL-Library"
  15.144 +    "HOL-Computational_Algebra"
  15.145    theories [document = false]
  15.146      "~~/src/HOL/Library/Code_Target_Numeral"
  15.147      "~~/src/HOL/Library/Monad_Syntax"
  15.148 @@ -445,8 +478,8 @@
  15.149    *}
  15.150    options [print_mode = "no_brackets",
  15.151      parallel_proofs = 0, quick_and_dirty = false]
  15.152 -  theories [document = false]
  15.153 -    "~~/src/HOL/Library/Code_Target_Int"
  15.154 +  sessions
  15.155 +    "HOL-Library"
  15.156    theories
  15.157      Eta
  15.158      StrongNorm
  15.159 @@ -473,6 +506,8 @@
  15.160      machine and a specification of its bytecode verifier and a lightweight
  15.161      bytecode verifier, including proofs of type-safety.
  15.162    *}
  15.163 +  sessions
  15.164 +    "HOL-Library"
  15.165    theories [document = false]
  15.166      "~~/src/HOL/Library/While_Combinator"
  15.167    theories
  15.168 @@ -542,6 +577,9 @@
  15.169    description {*
  15.170      Miscellaneous examples for Higher-Order Logic.
  15.171    *}
  15.172 +  sessions
  15.173 +    "HOL-Library"
  15.174 +    "HOL-Number_Theory"
  15.175    theories [document = false]
  15.176      "~~/src/HOL/Library/State_Monad"
  15.177      Code_Binary_Nat_examples
  15.178 @@ -638,6 +676,9 @@
  15.179      Miscellaneous Isabelle/Isar examples.
  15.180    *}
  15.181    options [quick_and_dirty]
  15.182 +  sessions
  15.183 +    "HOL-Library"
  15.184 +    "HOL-Computational_Algebra"
  15.185    theories [document = false]
  15.186      "~~/src/HOL/Library/Lattice_Syntax"
  15.187      "../Computational_Algebra/Primes"
  15.188 @@ -677,8 +718,12 @@
  15.189    description {*
  15.190      Verification of the SET Protocol.
  15.191    *}
  15.192 -  theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
  15.193 -  theories SET_Protocol
  15.194 +  sessions
  15.195 +    "HOL-Library"
  15.196 +  theories [document = false]
  15.197 +    "~~/src/HOL/Library/Nat_Bijection"
  15.198 +  theories
  15.199 +    SET_Protocol
  15.200    document_files "root.tex"
  15.201  
  15.202  session "HOL-Matrix_LP" in Matrix_LP = HOL +
  15.203 @@ -726,6 +771,8 @@
  15.204      ATP_Problem_Import
  15.205  
  15.206  session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
  15.207 +  sessions
  15.208 +    "HOL-Library"
  15.209    theories [document = false]
  15.210      "~~/src/HOL/Library/Countable"
  15.211      "~~/src/HOL/Library/Permutation"
  15.212 @@ -738,9 +785,9 @@
  15.213  
  15.214  session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
  15.215    theories
  15.216 -    "Dining_Cryptographers"
  15.217 -    "Koepf_Duermuth_Countermeasure"
  15.218 -    "Measure_Not_CCC"
  15.219 +    Dining_Cryptographers
  15.220 +    Koepf_Duermuth_Countermeasure
  15.221 +    Measure_Not_CCC
  15.222  
  15.223  session "HOL-Nominal" in Nominal = HOL +
  15.224    options [document = false]
  15.225 @@ -852,7 +899,10 @@
  15.226  
  15.227  session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
  15.228    options [document = false]
  15.229 -  theories NSPrimes
  15.230 +  sessions
  15.231 +    "HOL-Computational_Algebra"
  15.232 +  theories
  15.233 +    NSPrimes
  15.234  
  15.235  session "HOL-Mirabelle" in Mirabelle = HOL +
  15.236    options [document = false]
  15.237 @@ -989,6 +1039,8 @@
  15.238      Author:     Cezary Kaliszyk and Christian Urban
  15.239    *}
  15.240    options [document = false]
  15.241 +  sessions
  15.242 +    "HOL-Library"
  15.243    theories
  15.244      DList
  15.245      Quotient_FSet
  15.246 @@ -1042,6 +1094,8 @@
  15.247  
  15.248      HOLCF -- a semantic extension of HOL by the LCF logic.
  15.249    *}
  15.250 +  sessions
  15.251 +    "HOL-Library"
  15.252    theories [document = false]
  15.253      "~~/src/HOL/Library/Nat_Bijection"
  15.254      "~~/src/HOL/Library/Countable"
  15.255 @@ -1121,7 +1175,7 @@
  15.256      finite and infinite sequences.
  15.257    *}
  15.258    options [document = false]
  15.259 -  theories "Abstraction"
  15.260 +  theories Abstraction
  15.261  
  15.262  session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  15.263    description {*
    16.1 --- a/src/Pure/Admin/build_doc.scala	Thu Apr 20 16:21:29 2017 +0200
    16.2 +++ b/src/Pure/Admin/build_doc.scala	Fri Apr 21 20:36:20 2017 +0200
    16.3 @@ -24,11 +24,11 @@
    16.4    {
    16.5      val selection =
    16.6        for {
    16.7 -        (name, info) <- Sessions.load(options).build_topological_order
    16.8 +        info <- Sessions.load(options).build_topological_order
    16.9          if info.groups.contains("doc")
   16.10          doc = info.options.string("document_variants")
   16.11          if all_docs || docs.contains(doc)
   16.12 -      } yield (doc, name)
   16.13 +      } yield (doc, info.name)
   16.14  
   16.15      val selected_docs = selection.map(_._1)
   16.16      val sessions = selection.map(_._2)
    17.1 --- a/src/Pure/General/symbol.scala	Thu Apr 20 16:21:29 2017 +0200
    17.2 +++ b/src/Pure/General/symbol.scala	Fri Apr 21 20:36:20 2017 +0200
    17.3 @@ -216,7 +216,6 @@
    17.4          { case (List(a), Nil) => File(a) }))
    17.5      }
    17.6  
    17.7 -
    17.8      def apply(text: CharSequence): Text_Chunk =
    17.9        new Text_Chunk(Text.Range(0, text.length), Index(text))
   17.10    }
    18.1 --- a/src/Pure/Isar/token.scala	Thu Apr 20 16:21:29 2017 +0200
    18.2 +++ b/src/Pure/Isar/token.scala	Fri Apr 21 20:36:20 2017 +0200
    18.3 @@ -152,6 +152,19 @@
    18.4    val newline: Token = explode(Keyword.Keywords.empty, "\n").head
    18.5  
    18.6  
    18.7 +  /* names */
    18.8 +
    18.9 +  def read_name(keywords: Keyword.Keywords, inp: CharSequence): Option[Token] =
   18.10 +    explode(keywords, inp) match {
   18.11 +      case List(tok) if tok.is_name => Some(tok)
   18.12 +      case _ => None
   18.13 +    }
   18.14 +
   18.15 +  def quote_name(keywords: Keyword.Keywords, name: String): String =
   18.16 +    if (read_name(keywords, name).isDefined) name
   18.17 +    else quote(name.replace("\"", "\\\""))
   18.18 +
   18.19 +
   18.20    /* implode */
   18.21  
   18.22    def implode(toks: List[Token]): String =
    19.1 --- a/src/Pure/ML/ml_process.scala	Thu Apr 20 16:21:29 2017 +0200
    19.2 +++ b/src/Pure/ML/ml_process.scala	Fri Apr 21 20:36:20 2017 +0200
    19.3 @@ -99,8 +99,8 @@
    19.4              ML_Syntax.print_list(
    19.5                ML_Syntax.print_pair(
    19.6                  ML_Syntax.print_string, ML_Syntax.print_string))(table)
    19.7 -          List("Resources.init_session_base {default_qualifier = \"\"" +
    19.8 -            ", global_theories = " + print_table(base.global_theories.toList) +
    19.9 +          List("Resources.init_session_base" +
   19.10 +            " {global_theories = " + print_table(base.global_theories.toList) +
   19.11              ", loaded_theories = " + print_table(base.loaded_theories.toList) +
   19.12              ", known_theories = " + print_table(base.dest_known_theories) + "}")
   19.13        }
    20.1 --- a/src/Pure/PIDE/command.scala	Thu Apr 20 16:21:29 2017 +0200
    20.2 +++ b/src/Pure/PIDE/command.scala	Fri Apr 21 20:36:20 2017 +0200
    20.3 @@ -520,7 +520,7 @@
    20.4      Text.Range(0,
    20.5        (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
    20.6  
    20.7 -  def source(range: Text.Range): String = source.substring(range.start, range.stop)
    20.8 +  def source(range: Text.Range): String = range.substring(source)
    20.9  
   20.10  
   20.11    /* accumulated results */
    21.1 --- a/src/Pure/PIDE/line.scala	Thu Apr 20 16:21:29 2017 +0200
    21.2 +++ b/src/Pure/PIDE/line.scala	Fri Apr 21 20:36:20 2017 +0200
    21.3 @@ -123,8 +123,7 @@
    21.4      lazy val text: String = Document.text(lines)
    21.5  
    21.6      def try_get_text(range: Text.Range): Option[String] =
    21.7 -      if (text_range.contains(range)) Some(text.substring(range.start, range.stop))
    21.8 -      else None
    21.9 +      if (text_range.contains(range)) Some(range.substring(text)) else None
   21.10  
   21.11      override def toString: String = text
   21.12  
    22.1 --- a/src/Pure/PIDE/protocol.ML	Thu Apr 20 16:21:29 2017 +0200
    22.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Apr 21 20:36:20 2017 +0200
    22.3 @@ -19,13 +19,12 @@
    22.4  
    22.5  val _ =
    22.6    Isabelle_Process.protocol_command "Prover.session_base"
    22.7 -    (fn [default_qualifier, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
    22.8 +    (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
    22.9        let
   22.10          val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
   22.11        in
   22.12          Resources.init_session_base
   22.13 -          {default_qualifier = default_qualifier,
   22.14 -           global_theories = decode_table global_theories_yxml,
   22.15 +          {global_theories = decode_table global_theories_yxml,
   22.16             loaded_theories = decode_table loaded_theories_yxml,
   22.17             known_theories = decode_table known_theories_yxml}
   22.18        end);
    23.1 --- a/src/Pure/PIDE/protocol.scala	Thu Apr 20 16:21:29 2017 +0200
    23.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Apr 21 20:36:20 2017 +0200
    23.3 @@ -312,7 +312,6 @@
    23.4  
    23.5    def session_base(resources: Resources): Unit =
    23.6      protocol_command("Prover.session_base",
    23.7 -      Symbol.encode(resources.default_qualifier),
    23.8        encode_table(resources.session_base.global_theories.toList),
    23.9        encode_table(resources.session_base.loaded_theories.toList),
   23.10        encode_table(resources.session_base.dest_known_theories))
    24.1 --- a/src/Pure/PIDE/resources.ML	Thu Apr 20 16:21:29 2017 +0200
    24.2 +++ b/src/Pure/PIDE/resources.ML	Fri Apr 21 20:36:20 2017 +0200
    24.3 @@ -6,13 +6,12 @@
    24.4  
    24.5  signature RESOURCES =
    24.6  sig
    24.7 +  val default_qualifier: string
    24.8    val init_session_base:
    24.9 -    {default_qualifier: string,
   24.10 -     global_theories: (string * string) list,
   24.11 +    {global_theories: (string * string) list,
   24.12       loaded_theories: (string * string) list,
   24.13       known_theories: (string * string) list} -> unit
   24.14    val finish_session_base: unit -> unit
   24.15 -  val default_qualifier: unit -> string
   24.16    val global_theory: string -> string option
   24.17    val loaded_theory: string -> string option
   24.18    val known_theory: string -> Path.T option
   24.19 @@ -37,36 +36,32 @@
   24.20  
   24.21  (* session base *)
   24.22  
   24.23 +val default_qualifier = "Draft";
   24.24 +
   24.25  val empty_session_base =
   24.26 -  {default_qualifier = "Draft",
   24.27 -   global_theories = Symtab.empty: string Symtab.table,
   24.28 +  {global_theories = Symtab.empty: string Symtab.table,
   24.29     loaded_theories = Symtab.empty: string Symtab.table,
   24.30     known_theories = Symtab.empty: Path.T Symtab.table};
   24.31  
   24.32  val global_session_base =
   24.33    Synchronized.var "Sessions.base" empty_session_base;
   24.34  
   24.35 -fun init_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
   24.36 +fun init_session_base {global_theories, loaded_theories, known_theories} =
   24.37    Synchronized.change global_session_base
   24.38      (fn _ =>
   24.39 -      {default_qualifier =
   24.40 -        if default_qualifier <> "" then default_qualifier
   24.41 -        else #default_qualifier empty_session_base,
   24.42 -       global_theories = Symtab.make global_theories,
   24.43 +      {global_theories = Symtab.make global_theories,
   24.44         loaded_theories = Symtab.make loaded_theories,
   24.45         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
   24.46  
   24.47  fun finish_session_base () =
   24.48    Synchronized.change global_session_base
   24.49      (fn {global_theories, loaded_theories, ...} =>
   24.50 -      {default_qualifier = #default_qualifier empty_session_base,
   24.51 -       global_theories = global_theories,
   24.52 +      {global_theories = global_theories,
   24.53         loaded_theories = loaded_theories,
   24.54         known_theories = #known_theories empty_session_base});
   24.55  
   24.56  fun get_session_base f = f (Synchronized.value global_session_base);
   24.57  
   24.58 -fun default_qualifier () = get_session_base #default_qualifier;
   24.59  fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
   24.60  fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
   24.61  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    25.1 --- a/src/Pure/PIDE/resources.scala	Thu Apr 20 16:21:29 2017 +0200
    25.2 +++ b/src/Pure/PIDE/resources.scala	Fri Apr 21 20:36:20 2017 +0200
    25.3 @@ -15,7 +15,6 @@
    25.4  
    25.5  class Resources(
    25.6    val session_base: Sessions.Base,
    25.7 -  val default_qualifier: String = Sessions.DRAFT,
    25.8    val log: Logger = No_Logger)
    25.9  {
   25.10    val thy_info = new Thy_Info(this)
   25.11 @@ -93,8 +92,8 @@
   25.12          }
   25.13      }
   25.14  
   25.15 -  def import_name(node_name: Document.Node.Name, s: String): Document.Node.Name =
   25.16 -    import_name(theory_qualifier(node_name), node_name.master_dir, s)
   25.17 +  def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
   25.18 +    import_name(theory_qualifier(name), name.master_dir, s)
   25.19  
   25.20    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   25.21    {
    26.1 --- a/src/Pure/PIDE/text.scala	Thu Apr 20 16:21:29 2017 +0200
    26.2 +++ b/src/Pure/PIDE/text.scala	Fri Apr 21 20:36:20 2017 +0200
    26.3 @@ -71,6 +71,8 @@
    26.4      def try_join(that: Range): Option[Range] =
    26.5        if (this apart that) None
    26.6        else Some(Range(this.start min that.start, this.stop max that.stop))
    26.7 +
    26.8 +    def substring(text: String): String = text.substring(start, stop)
    26.9    }
   26.10  
   26.11  
    27.1 --- a/src/Pure/System/isabelle_tool.scala	Thu Apr 20 16:21:29 2017 +0200
    27.2 +++ b/src/Pure/System/isabelle_tool.scala	Fri Apr 21 20:36:20 2017 +0200
    27.3 @@ -115,6 +115,7 @@
    27.4        Remote_DMG.isabelle_tool,
    27.5        Update_Cartouches.isabelle_tool,
    27.6        Update_Header.isabelle_tool,
    27.7 +      Update_Imports.isabelle_tool,
    27.8        Update_Then.isabelle_tool,
    27.9        Update_Theorems.isabelle_tool,
   27.10        isabelle.vscode.Build_VSCode.isabelle_tool,
    28.1 --- a/src/Pure/Thy/sessions.scala	Thu Apr 20 16:21:29 2017 +0200
    28.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 21 20:36:20 2017 +0200
    28.3 @@ -81,6 +81,9 @@
    28.4        copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
    28.5          theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
    28.6          files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
    28.7 +
    28.8 +    def get_file(file: JFile): Option[Document.Node.Name] =
    28.9 +      files.getOrElse(file.getCanonicalFile, Nil).headOption
   28.10    }
   28.11  
   28.12    object Base
   28.13 @@ -95,6 +98,7 @@
   28.14    }
   28.15  
   28.16    sealed case class Base(
   28.17 +    imports: Option[Base] = None,
   28.18      global_theories: Map[String, String] = Map.empty,
   28.19      loaded_theories: Map[String, String] = Map.empty,
   28.20      known: Known = Known.empty,
   28.21 @@ -103,6 +107,8 @@
   28.22      sources: List[(Path, SHA1.Digest)] = Nil,
   28.23      session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
   28.24    {
   28.25 +    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
   28.26 +
   28.27      def platform_path: Base = copy(known = known.platform_path)
   28.28  
   28.29      def loaded_theory(name: Document.Node.Name): Boolean =
   28.30 @@ -111,9 +117,6 @@
   28.31      def known_theory(name: String): Option[Document.Node.Name] =
   28.32        known.theories.get(name)
   28.33  
   28.34 -    def known_file(file: JFile): Option[Document.Node.Name] =
   28.35 -      known.files.getOrElse(file.getCanonicalFile, Nil).headOption
   28.36 -
   28.37      def dest_known_theories: List[(String, String)] =
   28.38        for ((theory, node_name) <- known.theories.toList)
   28.39          yield (theory, node_name.node)
   28.40 @@ -137,7 +140,7 @@
   28.41    {
   28.42      val session_bases =
   28.43        (Map.empty[String, Base] /: sessions.imports_topological_order)({
   28.44 -        case (session_bases, (session_name, info)) =>
   28.45 +        case (session_bases, info) =>
   28.46            if (progress.stopped) throw Exn.Interrupt()
   28.47  
   28.48            try {
   28.49 @@ -150,22 +153,21 @@
   28.50                parent_base.copy(known =
   28.51                  Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
   28.52  
   28.53 -            val resources = new Resources(imports_base,
   28.54 -              default_qualifier = info.theory_qualifier(session_name))
   28.55 +            val resources = new Resources(imports_base)
   28.56  
   28.57              if (verbose || list_files) {
   28.58                val groups =
   28.59                  if (info.groups.isEmpty) ""
   28.60                  else info.groups.mkString(" (", " ", ")")
   28.61 -              progress.echo("Session " + info.chapter + "/" + session_name + groups)
   28.62 +              progress.echo("Session " + info.chapter + "/" + info.name + groups)
   28.63              }
   28.64  
   28.65              val thy_deps =
   28.66              {
   28.67                val root_theories =
   28.68                  info.theories.flatMap({ case (_, thys) =>
   28.69 -                  thys.map(thy =>
   28.70 -                    (resources.import_name(session_name, info.dir.implode, thy), info.pos))
   28.71 +                  thys.map({ case (thy, pos) =>
   28.72 +                    (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos) })
   28.73                  })
   28.74                val thy_deps = resources.thy_info.dependencies(root_theories)
   28.75  
   28.76 @@ -181,7 +183,7 @@
   28.77              val loaded_files =
   28.78                if (inlined_files) {
   28.79                  val pure_files =
   28.80 -                  if (is_pure(session_name)) {
   28.81 +                  if (is_pure(info.name)) {
   28.82                      val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
   28.83                      val files =
   28.84                        roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
   28.85 @@ -211,10 +213,10 @@
   28.86  
   28.87                def node(name: Document.Node.Name): Graph_Display.Node =
   28.88                {
   28.89 -                val session = resources.theory_qualifier(name)
   28.90 -                if (session == session_name)
   28.91 +                val qualifier = resources.theory_qualifier(name)
   28.92 +                if (qualifier == info.theory_qualifier)
   28.93                    Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
   28.94 -                else session_node(session)
   28.95 +                else session_node(qualifier)
   28.96                }
   28.97  
   28.98                val imports_subgraph =
   28.99 @@ -238,7 +240,8 @@
  28.100              }
  28.101  
  28.102              val base =
  28.103 -              Base(global_theories = global_theories,
  28.104 +              Base(imports = Some(imports_base),
  28.105 +                global_theories = global_theories,
  28.106                  loaded_theories = thy_deps.loaded_theories,
  28.107                  known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
  28.108                  keywords = thy_deps.keywords,
  28.109 @@ -246,12 +249,12 @@
  28.110                  sources = all_files.map(p => (p, SHA1.digest(p.file))),
  28.111                  session_graph = session_graph)
  28.112  
  28.113 -            session_bases + (session_name -> base)
  28.114 +            session_bases + (info.name -> base)
  28.115            }
  28.116            catch {
  28.117              case ERROR(msg) =>
  28.118                cat_error(msg, "The error(s) above occurred in session " +
  28.119 -                quote(session_name) + Position.here(info.pos))
  28.120 +                quote(info.name) + Position.here(info.pos))
  28.121            }
  28.122        })
  28.123  
  28.124 @@ -283,6 +286,7 @@
  28.125    /* cumulative session info */
  28.126  
  28.127    sealed case class Info(
  28.128 +    name: String,
  28.129      chapter: String,
  28.130      select: Boolean,
  28.131      pos: Position.T,
  28.132 @@ -292,7 +296,7 @@
  28.133      description: String,
  28.134      options: Options,
  28.135      imports: List[String],
  28.136 -    theories: List[(Options, List[String])],
  28.137 +    theories: List[(Options, List[(String, Position.T)])],
  28.138      global_theories: List[String],
  28.139      files: List[Path],
  28.140      document_files: List[(Path, Path)],
  28.141 @@ -300,9 +304,9 @@
  28.142    {
  28.143      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
  28.144  
  28.145 -    def theory_qualifier(default_qualifier: String): String =
  28.146 +    def theory_qualifier: String =
  28.147        options.string("theory_qualifier") match {
  28.148 -        case "" => default_qualifier
  28.149 +        case "" => name
  28.150          case qualifier => qualifier
  28.151        }
  28.152    }
  28.153 @@ -310,6 +314,7 @@
  28.154    object Selection
  28.155    {
  28.156      val empty: Selection = Selection()
  28.157 +    val all: Selection = Selection(all_sessions = true)
  28.158    }
  28.159  
  28.160    sealed case class Selection(
  28.161 @@ -416,10 +421,11 @@
  28.162      def global_theories: Map[String, String] =
  28.163        (Thy_Header.bootstrap_global_theories.toMap /:
  28.164          (for {
  28.165 -          (session_name, (info, _)) <- imports_graph.iterator
  28.166 -          thy <- info.global_theories.iterator } yield (thy, session_name, info)))({
  28.167 -            case (global, (thy, session_name, info)) =>
  28.168 -              val qualifier = info.theory_qualifier(session_name)
  28.169 +          (_, (info, _)) <- imports_graph.iterator
  28.170 +          thy <- info.global_theories.iterator }
  28.171 +         yield (thy, info)))({
  28.172 +            case (global, (thy, info)) =>
  28.173 +              val qualifier = info.theory_qualifier
  28.174                global.get(thy) match {
  28.175                  case Some(qualifier1) if qualifier != qualifier1 =>
  28.176                    error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
  28.177 @@ -440,11 +446,11 @@
  28.178      def build_descendants(names: List[String]): List[String] =
  28.179        build_graph.all_succs(names)
  28.180  
  28.181 -    def build_topological_order: List[(String, Info)] =
  28.182 -      build_graph.topological_order.map(name => (name, apply(name)))
  28.183 +    def build_topological_order: List[Info] =
  28.184 +      build_graph.topological_order.map(apply(_))
  28.185  
  28.186 -    def imports_topological_order: List[(String, Info)] =
  28.187 -      imports_graph.topological_order.map(name => (name, apply(name)))
  28.188 +    def imports_topological_order: List[Info] =
  28.189 +      imports_graph.topological_order.map(apply(_))
  28.190  
  28.191      override def toString: String =
  28.192        imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
  28.193 @@ -491,7 +497,7 @@
  28.194        description: String,
  28.195        options: List[Options.Spec],
  28.196        imports: List[String],
  28.197 -      theories: List[(List[Options.Spec], List[(String, Boolean)])],
  28.198 +      theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
  28.199        files: List[String],
  28.200        document_files: List[(String, String)]) extends Entry
  28.201  
  28.202 @@ -515,7 +521,7 @@
  28.203          ($$$("(") ~! $$$(GLOBAL) ~ $$$(")")) ^^ { case _ => true } | success(false)
  28.204  
  28.205        val theory_entry =
  28.206 -        theory_name ~ global ^^ { case x ~ y => (x, y) }
  28.207 +        position(theory_name) ~ global ^^ { case x ~ y => (x, y) }
  28.208  
  28.209        val theories =
  28.210          $$$(THEORIES) ~!
  28.211 @@ -561,11 +567,12 @@
  28.212              entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
  28.213  
  28.214            val global_theories =
  28.215 -            for { (_, thys) <- entry.theories; (thy, global) <- thys if global }
  28.216 +            for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
  28.217              yield {
  28.218                val thy_name = Path.explode(thy).expand.base.implode
  28.219                if (Long_Name.is_qualified(thy_name))
  28.220 -                error("Bad qualified name for global theory " + quote(thy_name))
  28.221 +                error("Bad qualified name for global theory " +
  28.222 +                  quote(thy_name) + Position.here(pos))
  28.223                else thy_name
  28.224              }
  28.225  
  28.226 @@ -578,9 +585,9 @@
  28.227                entry.imports, entry.theories, entry.files, entry.document_files).toString)
  28.228  
  28.229            val info =
  28.230 -            Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
  28.231 -              entry.parent, entry.description, session_options, entry.imports, theories,
  28.232 -              global_theories, files, document_files, meta_digest)
  28.233 +            Info(name, entry_chapter, select, entry.pos, entry.groups,
  28.234 +              dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
  28.235 +              entry.imports, theories, global_theories, files, document_files, meta_digest)
  28.236  
  28.237            (name, info)
  28.238          }
    29.1 --- a/src/Pure/Thy/thy_header.scala	Thu Apr 20 16:21:29 2017 +0200
    29.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Apr 21 20:36:20 2017 +0200
    29.3 @@ -81,6 +81,9 @@
    29.4    private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    29.5    private val Import_Name = new Regex(""".*?([^/\\:]+)""")
    29.6  
    29.7 +  def is_base_name(s: String): Boolean =
    29.8 +    s != "" && !s.exists("/\\:".contains(_))
    29.9 +
   29.10    def import_name(s: String): String =
   29.11      s match { case Import_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
   29.12  
   29.13 @@ -153,7 +156,7 @@
   29.14  
   29.15    /* read -- lazy scanning */
   29.16  
   29.17 -  def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
   29.18 +  private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) =
   29.19    {
   29.20      val token = Token.Parsers.token(bootstrap_keywords)
   29.21      def make_tokens(in: Reader[Char]): Stream[Token] =
   29.22 @@ -162,14 +165,30 @@
   29.23          case _ => Stream.empty
   29.24        }
   29.25  
   29.26 -    val tokens =
   29.27 -      if (strict) make_tokens(reader)
   29.28 -      else make_tokens(reader).dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
   29.29 +    val all_tokens = make_tokens(reader)
   29.30 +    val drop_tokens =
   29.31 +      if (strict) Nil
   29.32 +      else all_tokens.takeWhile(tok => !tok.is_command(Thy_Header.THEORY)).toList
   29.33  
   29.34 +    val tokens = all_tokens.drop(drop_tokens.length)
   29.35      val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList
   29.36      val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList
   29.37  
   29.38 -    parse(commit(header), Token.reader(tokens1 ::: tokens2, start)) match {
   29.39 +    (drop_tokens, tokens1 ::: tokens2)
   29.40 +  }
   29.41 +
   29.42 +  def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
   29.43 +  {
   29.44 +    val (_, tokens0) = read_tokens(reader, true)
   29.45 +    val text =
   29.46 +      if (reader.isInstanceOf[Scan.Byte_Reader])
   29.47 +        UTF8.decode_permissive(Token.implode(tokens0))
   29.48 +      else Token.implode(tokens0)
   29.49 +
   29.50 +    val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
   29.51 +    val pos = (start /: drop_tokens)(_.advance(_))
   29.52 +
   29.53 +    parse(commit(header), Token.reader(tokens, pos)) match {
   29.54        case Success(result, _) => result
   29.55        case bad => error(bad.toString)
   29.56      }
    30.1 --- a/src/Pure/Thy/thy_info.ML	Thu Apr 20 16:21:29 2017 +0200
    30.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Apr 21 20:36:20 2017 +0200
    30.3 @@ -408,7 +408,7 @@
    30.4  fun use_thy name =
    30.5    use_theories
    30.6      {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
    30.7 -     qualifier = Resources.default_qualifier (), master_dir = Path.current}
    30.8 +     qualifier = Resources.default_qualifier, master_dir = Path.current}
    30.9      [(name, Position.none)];
   30.10  
   30.11  
    31.1 --- a/src/Pure/Tools/build.ML	Thu Apr 20 16:21:29 2017 +0200
    31.2 +++ b/src/Pure/Tools/build.ML	Fri Apr 21 20:36:20 2017 +0200
    31.3 @@ -153,13 +153,14 @@
    31.4  fun decode_args yxml =
    31.5    let
    31.6      open XML.Decode;
    31.7 +    val position = Position.of_properties o properties;
    31.8      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
    31.9        (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
   31.10        (theories, (global_theories, (loaded_theories, known_theories)))))))))))))) =
   31.11        pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
   31.12          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
   31.13            (pair string
   31.14 -            (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
   31.15 +            (pair (((list (pair Options.decode (list (pair string position))))))
   31.16                (pair (list (pair string string))
   31.17                  (pair (list (pair string string)) (list (pair string string)))))))))))))))
   31.18        (YXML.parse_body yxml);
   31.19 @@ -181,8 +182,7 @@
   31.20  
   31.21      val _ =
   31.22        Resources.init_session_base
   31.23 -        {default_qualifier = name,
   31.24 -         global_theories = global_theories,
   31.25 +        {global_theories = global_theories,
   31.26           loaded_theories = loaded_theories,
   31.27           known_theories = known_theories};
   31.28  
    32.1 --- a/src/Pure/Tools/build.scala	Thu Apr 20 16:21:29 2017 +0200
    32.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 21 20:36:20 2017 +0200
    32.3 @@ -203,7 +203,7 @@
    32.4                pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
    32.5                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    32.6                  pair(string, pair(string, pair(string, pair(Path.encode,
    32.7 -                pair(list(pair(Options.encode, list(string))),
    32.8 +                pair(list(pair(Options.encode, list(pair(string, properties)))),
    32.9                  pair(list(pair(string, string)), pair(list(pair(string, string)),
   32.10                  list(pair(string, string))))))))))))))))(
   32.11                (Symbol.codes, (command_timings, (do_output, (verbose,
   32.12 @@ -223,8 +223,7 @@
   32.13              ML_Syntax.print_string0(File.platform_path(output))
   32.14  
   32.15          if (pide && !Sessions.is_pure(name)) {
   32.16 -          val resources =
   32.17 -            new Resources(deps(parent), default_qualifier = info.theory_qualifier(name))
   32.18 +          val resources = new Resources(deps(parent))
   32.19            val session = new Session(options, resources)
   32.20            val handler = new Handler(progress, session, name)
   32.21            session.init_protocol_handler(handler)
    33.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.2 +++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 20:36:20 2017 +0200
    33.3 @@ -0,0 +1,206 @@
    33.4 +/*  Title:      Pure/Tools/update_imports.scala
    33.5 +    Author:     Makarius
    33.6 +
    33.7 +Update theory imports to use session qualifiers.
    33.8 +*/
    33.9 +
   33.10 +package isabelle
   33.11 +
   33.12 +
   33.13 +import java.io.{File => JFile}
   33.14 +
   33.15 +
   33.16 +object Update_Imports
   33.17 +{
   33.18 +  /* update imports */
   33.19 +
   33.20 +  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
   33.21 +  {
   33.22 +    def edits: List[Text.Edit] =
   33.23 +      Text.Edit.replace(range.start, old_text, new_text)
   33.24 +
   33.25 +    override def toString: String =
   33.26 +      range.toString + ": " + old_text + " -> " + new_text
   33.27 +  }
   33.28 +
   33.29 +  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
   33.30 +    : Option[(JFile, Update)] =
   33.31 +  {
   33.32 +    val file =
   33.33 +      pos match {
   33.34 +        case Position.File(file) => Path.explode(file).file.getCanonicalFile
   33.35 +        case _ => error("Missing file in position" + Position.here(pos))
   33.36 +      }
   33.37 +
   33.38 +    val text = File.read(file)
   33.39 +
   33.40 +    val range =
   33.41 +      pos match {
   33.42 +        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
   33.43 +        case _ => error("Missing range in position" + Position.here(pos))
   33.44 +      }
   33.45 +
   33.46 +    Token.read_name(keywords, range.substring(text)) match {
   33.47 +      case Some(tok) =>
   33.48 +        val s1 = tok.source
   33.49 +        val s2 = Token.quote_name(keywords, update(tok.content))
   33.50 +        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
   33.51 +      case None => error("Name token expected" + Position.here(pos))
   33.52 +    }
   33.53 +  }
   33.54 +
   33.55 +  def update_imports(
   33.56 +    options: Options,
   33.57 +    progress: Progress = No_Progress,
   33.58 +    selection: Sessions.Selection = Sessions.Selection.empty,
   33.59 +    dirs: List[Path] = Nil,
   33.60 +    select_dirs: List[Path] = Nil,
   33.61 +    verbose: Boolean = false): List[(JFile, Update)] =
   33.62 +  {
   33.63 +    val full_sessions = Sessions.load(options, dirs, select_dirs)
   33.64 +    val (selected, selected_sessions) = full_sessions.selection(selection)
   33.65 +
   33.66 +    val deps =
   33.67 +      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
   33.68 +        global_theories = full_sessions.global_theories)
   33.69 +
   33.70 +    selected.flatMap(session_name =>
   33.71 +    {
   33.72 +      val info = full_sessions(session_name)
   33.73 +      val session_base = deps(session_name)
   33.74 +      val session_resources = new Resources(session_base)
   33.75 +      val imports_resources = new Resources(session_base.get_imports)
   33.76 +
   33.77 +      val local_theories =
   33.78 +        (for {
   33.79 +          (_, name) <- session_base.known.theories_local.iterator
   33.80 +          if session_resources.theory_qualifier(name) == info.theory_qualifier
   33.81 +        } yield name).toSet
   33.82 +
   33.83 +      def standard_import(qualifier: String, dir: String, s: String): String =
   33.84 +      {
   33.85 +        val name = imports_resources.import_name(qualifier, dir, s)
   33.86 +        val file = Path.explode(name.node).file
   33.87 +        val s1 =
   33.88 +          imports_resources.session_base.known.get_file(file) match {
   33.89 +            case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
   33.90 +              name1.theory
   33.91 +            case Some(name1) if Thy_Header.is_base_name(s) =>
   33.92 +              name1.theory_base_name
   33.93 +            case _ => s
   33.94 +          }
   33.95 +        val name2 = imports_resources.import_name(qualifier, dir, s1)
   33.96 +        if (name.node == name2.node) s1 else s
   33.97 +      }
   33.98 +
   33.99 +      val updates_root =
  33.100 +        for {
  33.101 +          (_, pos) <- info.theories.flatMap(_._2)
  33.102 +          upd <- update_name(Sessions.root_syntax.keywords, pos,
  33.103 +            standard_import(info.theory_qualifier, info.dir.implode, _))
  33.104 +        } yield upd
  33.105 +
  33.106 +      val updates_theories =
  33.107 +        for {
  33.108 +          (_, name) <- session_base.known.theories_local.toList
  33.109 +          (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
  33.110 +          upd <- update_name(session_base.syntax.keywords, pos,
  33.111 +            standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
  33.112 +        } yield upd
  33.113 +
  33.114 +      updates_root ::: updates_theories
  33.115 +    })
  33.116 +  }
  33.117 +
  33.118 +  def apply_updates(updates: List[(JFile, Update)])
  33.119 +  {
  33.120 +    val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
  33.121 +    val conflicts =
  33.122 +      file_updates.iterator_list.flatMap({ case (file, upds) =>
  33.123 +        Library.duplicates(upds.sortBy(_.range.start),
  33.124 +          (x: Update, y: Update) => x.range overlaps y.range) match
  33.125 +        {
  33.126 +          case Nil => None
  33.127 +          case bad => Some((file, bad))
  33.128 +        }
  33.129 +      })
  33.130 +    if (conflicts.nonEmpty)
  33.131 +      error(cat_lines(
  33.132 +        conflicts.map({ case (file, bad) =>
  33.133 +          "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
  33.134 +
  33.135 +    for ((file, upds) <- file_updates.iterator_list) {
  33.136 +      val edits =
  33.137 +        upds.sortBy(upd => - upd.range.start).flatMap(upd =>
  33.138 +          Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
  33.139 +      val new_text =
  33.140 +        (File.read(file) /: edits)({ case (text, edit) =>
  33.141 +          edit.edit(text, 0) match {
  33.142 +            case (None, text1) => text1
  33.143 +            case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
  33.144 +          }
  33.145 +        })
  33.146 +      File.write_backup2(Path.explode(File.standard_path(file)), new_text)
  33.147 +    }
  33.148 +  }
  33.149 +
  33.150 +
  33.151 +  /* Isabelle tool wrapper */
  33.152 +
  33.153 +  val isabelle_tool =
  33.154 +    Isabelle_Tool("update_imports", "update theory imports to use session qualifiers", args =>
  33.155 +    {
  33.156 +      var select_dirs: List[Path] = Nil
  33.157 +      var requirements = false
  33.158 +      var exclude_session_groups: List[String] = Nil
  33.159 +      var all_sessions = false
  33.160 +      var dirs: List[Path] = Nil
  33.161 +      var session_groups: List[String] = Nil
  33.162 +      var options = Options.init()
  33.163 +      var verbose = false
  33.164 +      var exclude_sessions: List[String] = Nil
  33.165 +
  33.166 +      val getopts = Getopts("""
  33.167 +Usage: isabelle update_imports [OPTIONS] [SESSIONS ...]
  33.168 +
  33.169 +  Options are:
  33.170 +    -D DIR       include session directory and select its sessions
  33.171 +    -R           operate on requirements of selected sessions
  33.172 +    -X NAME      exclude sessions from group NAME and all descendants
  33.173 +    -a           select all sessions
  33.174 +    -d DIR       include session directory
  33.175 +    -g NAME      select session group NAME
  33.176 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
  33.177 +    -v           verbose
  33.178 +    -x NAME      exclude session NAME and all descendants
  33.179 +
  33.180 +  Update theory imports to use session qualifiers.
  33.181 +
  33.182 +  Old versions of files are preserved by appending "~~".
  33.183 +""",
  33.184 +      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
  33.185 +      "R" -> (_ => requirements = true),
  33.186 +      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
  33.187 +      "a" -> (_ => all_sessions = true),
  33.188 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
  33.189 +      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
  33.190 +      "o:" -> (arg => options = options + arg),
  33.191 +      "v" -> (_ => verbose = true),
  33.192 +      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
  33.193 +
  33.194 +      val sessions = getopts(args)
  33.195 +      if (args.isEmpty) getopts.usage()
  33.196 +
  33.197 +      val selection =
  33.198 +        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
  33.199 +          exclude_sessions, session_groups, sessions)
  33.200 +
  33.201 +      val progress = new Console_Progress(verbose = verbose)
  33.202 +
  33.203 +      val updates =
  33.204 +        update_imports(options, progress = progress, selection = selection,
  33.205 +          dirs = dirs, select_dirs = select_dirs, verbose = verbose)
  33.206 +
  33.207 +      apply_updates(updates)
  33.208 +    })
  33.209 +}
    34.1 --- a/src/Pure/build-jars	Thu Apr 20 16:21:29 2017 +0200
    34.2 +++ b/src/Pure/build-jars	Fri Apr 21 20:36:20 2017 +0200
    34.3 @@ -143,6 +143,7 @@
    34.4    Tools/task_statistics.scala
    34.5    Tools/update_cartouches.scala
    34.6    Tools/update_header.scala
    34.7 +  Tools/update_imports.scala
    34.8    Tools/update_then.scala
    34.9    Tools/update_theorems.scala
   34.10    library.scala
    35.1 --- a/src/Tools/Code/code_scala.ML	Thu Apr 20 16:21:29 2017 +0200
    35.2 +++ b/src/Tools/Code/code_scala.ML	Fri Apr 21 20:36:20 2017 +0200
    35.3 @@ -465,7 +465,7 @@
    35.4        check = { env_var = "SCALA_HOME",
    35.5          make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
    35.6          make_command = fn _ =>
    35.7 -          "env JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' \"$SCALA_HOME/bin/scalac\" $ISABELLE_SCALAC_OPTIONS ROOT.scala" } })
    35.8 +          "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala" } })
    35.9    #> Code_Target.set_printings (Type_Constructor ("fun",
   35.10      [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   35.11        brackify_infix (1, R) fxy (
    36.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Apr 20 16:21:29 2017 +0200
    36.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Apr 21 20:36:20 2017 +0200
    36.3 @@ -61,9 +61,9 @@
    36.4    def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
    36.5  
    36.6    def node_name(file: JFile): Document.Node.Name =
    36.7 -    session_base.known_file(file) getOrElse {
    36.8 +    session_base.known.get_file(file) getOrElse {
    36.9        val node = file.getPath
   36.10 -      theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
   36.11 +      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
   36.12          case (true, theory) => Document.Node.Name.loaded_theory(theory)
   36.13          case (false, theory) =>
   36.14            val master_dir = if (theory == "") "" else file.getParent
    37.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Thu Apr 20 16:21:29 2017 +0200
    37.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Apr 21 20:36:20 2017 +0200
    37.3 @@ -97,7 +97,6 @@
    37.4    echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
    37.5    echo
    37.6    echo "  Options are:"
    37.7 -  echo "    -A           explore theory imports of all known sessions"
    37.8    echo "    -D NAME=X    set JVM system property"
    37.9    echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
   37.10    echo "    -R           open ROOT entry of logic session and use its parent"
   37.11 @@ -134,7 +133,6 @@
   37.12  
   37.13  # options
   37.14  
   37.15 -JEDIT_ALL_KNOWN=""
   37.16  BUILD_ONLY=false
   37.17  BUILD_JARS="jars"
   37.18  ML_PROCESS_POLICY=""
   37.19 @@ -147,12 +145,9 @@
   37.20  function getoptions()
   37.21  {
   37.22    OPTIND=1
   37.23 -  while getopts "AD:J:Rbd:fj:l:m:np:s" OPT
   37.24 +  while getopts "D:J:Rbd:fj:l:m:np:s" OPT
   37.25    do
   37.26      case "$OPT" in
   37.27 -      A)
   37.28 -        JEDIT_ALL_KNOWN="true"
   37.29 -        ;;
   37.30        D)
   37.31          JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
   37.32          ;;
   37.33 @@ -350,7 +345,7 @@
   37.34        classpath "$JAR"
   37.35      done
   37.36      export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
   37.37 -    exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALAC_OPTIONS -d dist/classes "${SOURCES[@]}"
   37.38 +    isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d dist/classes "${SOURCES[@]}"
   37.39    ) || fail "Failed to compile sources"
   37.40  
   37.41    cd dist/classes
   37.42 @@ -376,7 +371,7 @@
   37.43  
   37.44  if [ "$BUILD_ONLY" = false ]
   37.45  then
   37.46 -  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_ALL_KNOWN JEDIT_PRINT_MODE JEDIT_BUILD_MODE
   37.47 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
   37.48    export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
   37.49    classpath "$JEDIT_HOME/dist/jedit.jar"
   37.50    exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
    38.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 20 16:21:29 2017 +0200
    38.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Apr 21 20:36:20 2017 +0200
    38.3 @@ -176,7 +176,7 @@
    38.4      catch { case _: ArrayIndexOutOfBoundsException => None }
    38.5  
    38.6    def try_get_text(text: String, range: Text.Range): Option[String] =
    38.7 -    try { Some(text.substring(range.start, range.stop)) }
    38.8 +    try { Some(range.substring(text)) }
    38.9      catch { case _: IndexOutOfBoundsException => None }
   38.10  
   38.11  
    39.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 20 16:21:29 2017 +0200
    39.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri Apr 21 20:36:20 2017 +0200
    39.3 @@ -26,13 +26,13 @@
    39.4    /* document node name */
    39.5  
    39.6    def known_file(path: String): Option[Document.Node.Name] =
    39.7 -    JEdit_Lib.check_file(path).flatMap(session_base.known_file(_))
    39.8 +    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_))
    39.9  
   39.10    def node_name(path: String): Document.Node.Name =
   39.11      known_file(path) getOrElse {
   39.12        val vfs = VFSManager.getVFSForPath(path)
   39.13        val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
   39.14 -      theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
   39.15 +      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
   39.16          case (true, theory) => Document.Node.Name.loaded_theory(theory)
   39.17          case (false, theory) =>
   39.18            val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    40.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Apr 20 16:21:29 2017 +0200
    40.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Apr 21 20:36:20 2017 +0200
    40.3 @@ -77,8 +77,8 @@
    40.4    {
    40.5      val sessions = Sessions.load(options, dirs = session_dirs())
    40.6      val (main_sessions, other_sessions) =
    40.7 -      sessions.imports_topological_order.partition(p => p._2.groups.contains("main"))
    40.8 -    main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
    40.9 +      sessions.imports_topological_order.partition(info => info.groups.contains("main"))
   40.10 +    main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
   40.11    }
   40.12  
   40.13  
    41.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Apr 20 16:21:29 2017 +0200
    41.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Apr 21 20:36:20 2017 +0200
    41.3 @@ -74,9 +74,8 @@
    41.4      val session_name = JEdit_Sessions.session_name(options)
    41.5      val session_base =
    41.6        try {
    41.7 -        Sessions.session_base(options, session_name,
    41.8 -          dirs = JEdit_Sessions.session_dirs(),
    41.9 -          all_known = Isabelle_System.getenv("JEDIT_ALL_KNOWN") == "true")
   41.10 +        Sessions.session_base(
   41.11 +          options, session_name, dirs = JEdit_Sessions.session_dirs(), all_known = true)
   41.12        }
   41.13        catch { case ERROR(_) => Sessions.Base.pure(options) }
   41.14  
    42.1 --- a/src/ZF/ROOT	Thu Apr 20 16:21:29 2017 +0200
    42.2 +++ b/src/ZF/ROOT	Fri Apr 21 20:36:20 2017 +0200
    42.3 @@ -43,7 +43,8 @@
    42.4      (North-Holland, 1980)
    42.5    *}
    42.6    theories
    42.7 -    ZFC
    42.8 +    ZF (global)
    42.9 +    ZFC (global)
   42.10    document_files "root.tex"
   42.11  
   42.12  session "ZF-AC" (ZF) in AC = ZF +