tuned syntax;
authorwenzelm
Tue Apr 04 21:05:07 2017 +0200 (2017-04-04)
changeset 65374a5b38d8d3c1e
parent 65373 905ed0102c69
child 65375 35a85aa725e9
tuned syntax;
some official documentation;
src/Doc/System/Sessions.thy
src/FOL/ROOT
src/HOL/ROOT
src/Pure/ROOT
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Doc/System/Sessions.thy	Tue Apr 04 19:51:56 2017 +0200
     1.2 +++ b/src/Doc/System/Sessions.thy	Tue Apr 04 21:05:07 2017 +0200
     1.3 @@ -70,7 +70,9 @@
     1.4      ;
     1.5      value: @{syntax name} | @{syntax real}
     1.6      ;
     1.7 -    theories: @'theories' opts? ( @{syntax name} * )
     1.8 +    theory_entry: @{syntax name} ('(' @'global' ')')?
     1.9 +    ;
    1.10 +    theories: @'theories' opts? (theory_entry*)
    1.11      ;
    1.12      files: @'files' (@{syntax name}+)
    1.13      ;
    1.14 @@ -116,6 +118,11 @@
    1.15    of \isakeyword{theories} may be given. Options are only active for each
    1.16    \isakeyword{theories} block separately.
    1.17  
    1.18 +  A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated
    1.19 +  literally in other session specifications or theory imports. In contrast,
    1.20 +  the default is to qualify theory names by the session name, in order to
    1.21 +  ensure globally unique names in big session trees.
    1.22 +
    1.23    \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
    1.24    in the processing of this session. This should cover anything outside the
    1.25    formal content of the theory sources. In contrast, files that are loaded
     2.1 --- a/src/FOL/ROOT	Tue Apr 04 19:51:56 2017 +0200
     2.2 +++ b/src/FOL/ROOT	Tue Apr 04 21:05:07 2017 +0200
     2.3 @@ -15,9 +15,9 @@
     2.4  
     2.5      Michael Dummett, Elements of Intuitionism (Oxford, 1977)
     2.6    *}
     2.7 -  global_theories
     2.8 -    IFOL
     2.9 -    FOL
    2.10 +  theories
    2.11 +    IFOL (global)
    2.12 +    FOL (global)
    2.13    document_files "root.tex"
    2.14  
    2.15  session "FOL-ex" in ex = FOL +
     3.1 --- a/src/HOL/ROOT	Tue Apr 04 19:51:56 2017 +0200
     3.2 +++ b/src/HOL/ROOT	Tue Apr 04 21:05:07 2017 +0200
     3.3 @@ -4,9 +4,9 @@
     3.4    description {*
     3.5      Classical Higher-order Logic.
     3.6    *}
     3.7 -  global_theories
     3.8 -    Main
     3.9 -    Complex_Main
    3.10 +  theories
    3.11 +    Main (global)
    3.12 +    Complex_Main (global)
    3.13    files
    3.14      "Tools/Quickcheck/Narrowing_Engine.hs"
    3.15      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
     4.1 --- a/src/Pure/ROOT	Tue Apr 04 19:51:56 2017 +0200
     4.2 +++ b/src/Pure/ROOT	Tue Apr 04 21:05:07 2017 +0200
     4.3 @@ -5,7 +5,6 @@
     4.4      The Pure logical framework
     4.5    *}
     4.6    options [threads = 1]
     4.7 -  global_theories
     4.8 -    Pure
     4.9    theories
    4.10 +    Pure (global)
    4.11      ML_Bootstrap
     5.1 --- a/src/Pure/Thy/sessions.scala	Tue Apr 04 19:51:56 2017 +0200
     5.2 +++ b/src/Pure/Thy/sessions.scala	Tue Apr 04 21:05:07 2017 +0200
     5.3 @@ -80,10 +80,9 @@
     5.4              val thy_deps =
     5.5              {
     5.6                val root_theories =
     5.7 -                info.theories.flatMap({
     5.8 -                  case (_, _, thys) =>
     5.9 -                    thys.map(thy =>
    5.10 -                      (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
    5.11 +                info.theories.flatMap({ case (_, thys) =>
    5.12 +                  thys.map(thy =>
    5.13 +                    (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
    5.14                  })
    5.15                val thy_deps = resources.thy_info.dependencies(root_theories)
    5.16  
    5.17 @@ -176,21 +175,13 @@
    5.18      parent: Option[String],
    5.19      description: String,
    5.20      options: Options,
    5.21 -    theories: List[(Boolean, Options, List[Path])],
    5.22 +    theories: List[(Options, List[Path])],
    5.23 +    global_theories: List[String],
    5.24      files: List[Path],
    5.25      document_files: List[(Path, Path)],
    5.26      meta_digest: SHA1.Digest)
    5.27    {
    5.28      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    5.29 -
    5.30 -    def global_theories: List[String] =
    5.31 -      for { (global, _, paths) <- theories if global; path <- paths }
    5.32 -      yield {
    5.33 -        val name = path.base.implode
    5.34 -        if (Long_Name.is_qualified(name))
    5.35 -          error("Bad qualified name for global theory " + quote(name))
    5.36 -        else name
    5.37 -      }
    5.38    }
    5.39  
    5.40    object Tree
    5.41 @@ -306,18 +297,17 @@
    5.42    private val IN = "in"
    5.43    private val DESCRIPTION = "description"
    5.44    private val OPTIONS = "options"
    5.45 -  private val GLOBAL_THEORIES = "global_theories"
    5.46    private val THEORIES = "theories"
    5.47 +  private val GLOBAL = "global"
    5.48    private val FILES = "files"
    5.49    private val DOCUMENT_FILES = "document_files"
    5.50  
    5.51    lazy val root_syntax =
    5.52 -    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + IN +
    5.53 +    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
    5.54        (CHAPTER, Keyword.THY_DECL) +
    5.55        (SESSION, Keyword.THY_DECL) +
    5.56        (DESCRIPTION, Keyword.QUASI_COMMAND) +
    5.57        (OPTIONS, Keyword.QUASI_COMMAND) +
    5.58 -      (GLOBAL_THEORIES, Keyword.QUASI_COMMAND) +
    5.59        (THEORIES, Keyword.QUASI_COMMAND) +
    5.60        (FILES, Keyword.QUASI_COMMAND) +
    5.61        (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
    5.62 @@ -334,7 +324,7 @@
    5.63        parent: Option[String],
    5.64        description: String,
    5.65        options: List[Options.Spec],
    5.66 -      theories: List[(Boolean, List[Options.Spec], List[String])],
    5.67 +      theories: List[(List[Options.Spec], List[(String, Boolean)])],
    5.68        files: List[String],
    5.69        document_files: List[(String, String)]) extends Entry
    5.70  
    5.71 @@ -354,10 +344,16 @@
    5.72            { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
    5.73        val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
    5.74  
    5.75 +      val global =
    5.76 +        ($$$("(") ~! $$$(GLOBAL) ~ $$$(")")) ^^ { case _ => true } | success(false)
    5.77 +
    5.78 +      val theory_entry =
    5.79 +        theory_name ~ global ^^ { case x ~ y => (x, y) }
    5.80 +
    5.81        val theories =
    5.82 -        ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
    5.83 -          ((options | success(Nil)) ~ rep(theory_name)) ^^
    5.84 -          { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
    5.85 +        $$$(THEORIES) ~!
    5.86 +          ((options | success(Nil)) ~ rep(theory_entry)) ^^
    5.87 +          { case _ ~ (x ~ y) => (x, y) }
    5.88  
    5.89        val document_files =
    5.90          $$$(DOCUMENT_FILES) ~!
    5.91 @@ -394,8 +390,18 @@
    5.92            val session_options = options ++ entry.options
    5.93  
    5.94            val theories =
    5.95 -            entry.theories.map({ case (global, opts, thys) =>
    5.96 -              (global, session_options ++ opts, thys.map(Path.explode(_))) })
    5.97 +            entry.theories.map({ case (opts, thys) =>
    5.98 +              (session_options ++ opts, thys.map(thy => Path.explode(thy._1))) })
    5.99 +
   5.100 +          val global_theories =
   5.101 +            for { (_, thys) <- entry.theories; (thy, global) <- thys if global }
   5.102 +            yield {
   5.103 +              val thy_name = Path.explode(thy).expand.base.implode
   5.104 +              if (Long_Name.is_qualified(thy_name))
   5.105 +                error("Bad qualified name for global theory " + quote(thy_name))
   5.106 +              else thy_name
   5.107 +            }
   5.108 +
   5.109            val files = entry.files.map(Path.explode(_))
   5.110            val document_files =
   5.111              entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
   5.112 @@ -406,8 +412,8 @@
   5.113  
   5.114            val info =
   5.115              Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
   5.116 -              entry.parent, entry.description, session_options, theories, files,
   5.117 -              document_files, meta_digest)
   5.118 +              entry.parent, entry.description, session_options, theories, global_theories,
   5.119 +              files, document_files, meta_digest)
   5.120  
   5.121            (name, info)
   5.122          }
     6.1 --- a/src/Pure/Tools/build.scala	Tue Apr 04 19:51:56 2017 +0200
     6.2 +++ b/src/Pure/Tools/build.scala	Tue Apr 04 21:05:07 2017 +0200
     6.3 @@ -200,7 +200,6 @@
     6.4          val args_yxml =
     6.5            YXML.string_of_body(
     6.6              {
     6.7 -              val theories = info.theories.map(x => (x._2, x._3))
     6.8                import XML.Encode._
     6.9                pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
    6.10                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    6.11 @@ -209,7 +208,7 @@
    6.12                (Symbol.codes, (command_timings, (do_output, (verbose,
    6.13                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    6.14                  (parent, (info.chapter, (name, (Path.current,
    6.15 -                theories))))))))))))
    6.16 +                info.theories))))))))))))
    6.17              })
    6.18  
    6.19          val env =