support 'export_files' in session ROOT;
authorwenzelm
Sat May 26 19:40:02 2018 +0200 (13 months ago)
changeset 682927ca0c23179e6
parent 68291 1e1877cb9b3a
child 68293 2bc4e5d9cca6
support 'export_files' in session ROOT;
NEWS
src/Doc/System/Sessions.thy
src/Pure/Sessions.thy
src/Pure/Thy/sessions.ML
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Sat May 26 19:39:06 2018 +0200
     1.2 +++ b/NEWS	Sat May 26 19:40:02 2018 +0200
     1.3 @@ -372,8 +372,8 @@
     1.4  $ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
     1.5  "isabelle jedit -s" or "isabelle build -s").
     1.6  
     1.7 -* The command-line tool retrieves theory exports from the session build
     1.8 -database.
     1.9 +* The command-line tool "export" and 'export_files' in session ROOT
    1.10 +entries retrieve theory exports from the session build database.
    1.11  
    1.12  * The command-line tools "isabelle server" and "isabelle client" provide
    1.13  access to the Isabelle Server: it supports responsive session management
     2.1 --- a/src/Doc/System/Sessions.thy	Sat May 26 19:39:06 2018 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Sat May 26 19:40:02 2018 +0200
     2.3 @@ -54,7 +54,7 @@
     2.4  
     2.5      @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline>
     2.6        (@{syntax system_name} '+')? description? options? \<newline>
     2.7 -      (sessions?) (theories*) (document_files*)
     2.8 +      (sessions?) (theories*) (document_files*) \<newline> (export_files*)
     2.9      ;
    2.10      groups: '(' (@{syntax name} +) ')'
    2.11      ;
    2.12 @@ -75,6 +75,8 @@
    2.13      theory_entry: @{syntax system_name} ('(' @'global' ')')?
    2.14      ;
    2.15      document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
    2.16 +    ;
    2.17 +    export_files: @'export_files' ('(' dir ')')? (@{syntax name}+)
    2.18    \<close>}
    2.19  
    2.20    \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
    2.21 @@ -138,12 +140,14 @@
    2.22    directory to the document output directory, before formal document
    2.23    processing is started (see also \secref{sec:tool-document}). The local path
    2.24    structure of the \<open>files\<close> is preserved, which allows to reconstruct the
    2.25 -  original directory hierarchy of \<open>base_dir\<close>.
    2.26 +  original directory hierarchy of \<open>base_dir\<close>. The default \<open>base_dir\<close> is
    2.27 +  \<^verbatim>\<open>document\<close> within the session root directory.
    2.28  
    2.29 -  \<^descr> \isakeyword{document_files}~\<open>files\<close> abbreviates
    2.30 -  \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\
    2.31 -  document sources are taken from the base directory \<^verbatim>\<open>document\<close> within the
    2.32 -  session root directory.
    2.33 +  \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) patterns\<close> writes
    2.34 +  theory exports to the file-system: the \<open>target_dir\<close> specification is
    2.35 +  relative to the session root directory; its default is \<^verbatim>\<open>export\<close>. Exports
    2.36 +  are selected via \<open>patterns\<close> as in @{tool_ref export}
    2.37 +  (\secref{sec:tool-export}).
    2.38  \<close>
    2.39  
    2.40  
     3.1 --- a/src/Pure/Sessions.thy	Sat May 26 19:39:06 2018 +0200
     3.2 +++ b/src/Pure/Sessions.thy	Sat May 26 19:40:02 2018 +0200
     3.3 @@ -7,7 +7,8 @@
     3.4  theory Sessions
     3.5    imports Pure
     3.6    keywords "session" :: thy_decl
     3.7 -    and "description" "options" "sessions" "theories" "document_files" :: quasi_command
     3.8 +    and "description" "options" "sessions" "theories"
     3.9 +      "document_files" "export_files" :: quasi_command
    3.10      and "global"
    3.11  begin
    3.12  
     4.1 --- a/src/Pure/Thy/sessions.ML	Sat May 26 19:39:06 2018 +0200
     4.2 +++ b/src/Pure/Thy/sessions.ML	Sat May 26 19:40:02 2018 +0200
     4.3 @@ -27,15 +27,18 @@
     4.4  val theories =
     4.5    Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry);
     4.6  
     4.7 +val in_path =
     4.8 +  Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.position Parse.path --| Parse.$$$ ")");
     4.9 +
    4.10  val document_files =
    4.11    Parse.$$$ "document_files" |--
    4.12 -    Parse.!!!
    4.13 -      (Scan.optional
    4.14 -        (Parse.$$$ "(" |--
    4.15 -            Parse.!!! (Parse.$$$ "in" |-- Parse.position Parse.path --| Parse.$$$ ")"))
    4.16 -        ("document", Position.none)
    4.17 +    Parse.!!! (Scan.optional in_path ("document", Position.none)
    4.18        -- Scan.repeat1 (Parse.position Parse.path));
    4.19  
    4.20 +val export_files =
    4.21 +  Parse.$$$ "export_files" |--
    4.22 +    Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.name);
    4.23 +
    4.24  in
    4.25  
    4.26  val command_parser =
    4.27 @@ -49,9 +52,10 @@
    4.28        Scan.optional (Parse.$$$ "sessions" |--
    4.29          Parse.!!! (Scan.repeat1 (Parse.position Parse.session_name))) [] --
    4.30        Scan.repeat theories --
    4.31 -      Scan.repeat document_files))
    4.32 +      Scan.repeat document_files --
    4.33 +      Scan.repeat export_files))
    4.34    >> (fn (((session, _), dir),
    4.35 -          ((((((parent, descr), options), sessions), theories), document_files))) =>
    4.36 +          (((((((parent, descr), options), sessions), theories), document_files), export_files))) =>
    4.37      Toplevel.keep (fn state =>
    4.38        let
    4.39          val ctxt = Toplevel.context_of state;
    4.40 @@ -89,6 +93,10 @@
    4.41                val dir = Resources.check_dir ctxt session_dir doc_dir;
    4.42                val _ = List.app (ignore o Resources.check_file ctxt dir) doc_files;
    4.43              in () end);
    4.44 +
    4.45 +        val _ =
    4.46 +          export_files |> List.app (fn (export_dir, _) =>
    4.47 +            ignore (Resources.check_path ctxt session_dir export_dir));
    4.48        in () end));
    4.49  
    4.50  end;
     5.1 --- a/src/Pure/Thy/sessions.scala	Sat May 26 19:39:06 2018 +0200
     5.2 +++ b/src/Pure/Thy/sessions.scala	Sat May 26 19:40:02 2018 +0200
     5.3 @@ -428,7 +428,8 @@
     5.4                    options = Nil,
     5.5                    imports = info.deps,
     5.6                    theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
     5.7 -                  document_files = Nil))))
     5.8 +                  document_files = Nil,
     5.9 +                  export_files = Nil))))
    5.10          }
    5.11        }
    5.12        else (session, Nil)
    5.13 @@ -469,6 +470,7 @@
    5.14      theories: List[(Options, List[(String, Position.T)])],
    5.15      global_theories: List[String],
    5.16      document_files: List[(Path, Path)],
    5.17 +    export_files: List[(Path, List[String])],
    5.18      meta_digest: SHA1.Digest)
    5.19    {
    5.20      def deps: List[String] = parent.toList ::: imports
    5.21 @@ -520,13 +522,16 @@
    5.22        val document_files =
    5.23          entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    5.24  
    5.25 +      val export_files =
    5.26 +        entry.export_files.map({ case (dir, pats) => (Path.explode(dir), pats) })
    5.27 +
    5.28        val meta_digest =
    5.29          SHA1.digest((name, chapter, entry.parent, entry.options, entry.imports,
    5.30 -          entry.theories_no_position, conditions, entry.document_files).toString)
    5.31 +          entry.theories_no_position, conditions, entry.document_files, entry.export_files).toString)
    5.32  
    5.33        Info(name, chapter, dir_selected, entry.pos, entry.groups,
    5.34          dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
    5.35 -        entry.imports, theories, global_theories, document_files, meta_digest)
    5.36 +        entry.imports, theories, global_theories, document_files, export_files, meta_digest)
    5.37      }
    5.38      catch {
    5.39        case ERROR(msg) =>
    5.40 @@ -703,6 +708,7 @@
    5.41    private val THEORIES = "theories"
    5.42    private val GLOBAL = "global"
    5.43    private val DOCUMENT_FILES = "document_files"
    5.44 +  private val EXPORT_FILES = "export_files"
    5.45  
    5.46    val root_syntax =
    5.47      Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
    5.48 @@ -712,7 +718,8 @@
    5.49        (OPTIONS, Keyword.QUASI_COMMAND) +
    5.50        (SESSIONS, Keyword.QUASI_COMMAND) +
    5.51        (THEORIES, Keyword.QUASI_COMMAND) +
    5.52 -      (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
    5.53 +      (DOCUMENT_FILES, Keyword.QUASI_COMMAND) +
    5.54 +      (EXPORT_FILES, Keyword.QUASI_COMMAND)
    5.55  
    5.56    abstract class Entry
    5.57    sealed case class Chapter(name: String) extends Entry
    5.58 @@ -726,7 +733,8 @@
    5.59      options: List[Options.Spec],
    5.60      imports: List[String],
    5.61      theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
    5.62 -    document_files: List[(String, String)]) extends Entry
    5.63 +    document_files: List[(String, String)],
    5.64 +    export_files: List[(String, List[String])]) extends Entry
    5.65    {
    5.66      def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
    5.67        theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
    5.68 @@ -759,11 +767,15 @@
    5.69            ((options | success(Nil)) ~ rep1(theory_entry)) ^^
    5.70            { case _ ~ (x ~ y) => (x, y) }
    5.71  
    5.72 +      val in_path = $$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x }
    5.73 +
    5.74        val document_files =
    5.75          $$$(DOCUMENT_FILES) ~!
    5.76 -          (($$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^
    5.77 -              { case _ ~ (_ ~ x ~ _) => x } | success("document")) ~
    5.78 -            rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
    5.79 +          ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
    5.80 +
    5.81 +      val export_files =
    5.82 +        $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ rep1(name)) ^^
    5.83 +          { case _ ~ (x ~ y) => (x, y) }
    5.84  
    5.85        command(SESSION) ~!
    5.86          (position(session_name) ~
    5.87 @@ -775,9 +787,10 @@
    5.88                (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    5.89                (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
    5.90                rep(theories) ~
    5.91 -              (rep(document_files) ^^ (x => x.flatten))))) ^^
    5.92 -        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
    5.93 -            Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
    5.94 +              (rep(document_files) ^^ (x => x.flatten)) ~
    5.95 +              (rep(export_files))))) ^^
    5.96 +        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j))) =>
    5.97 +            Session_Entry(pos, a, b, c, d, e, f, g, h, i, j) }
    5.98      }
    5.99  
   5.100      def parse_root(path: Path): List[Entry] =
     6.1 --- a/src/Pure/Tools/build.scala	Sat May 26 19:39:06 2018 +0200
     6.2 +++ b/src/Pure/Tools/build.scala	Sat May 26 19:40:02 2018 +0200
     6.3 @@ -322,8 +322,15 @@
     6.4  
     6.5        Isabelle_System.rm_tree(export_tmp_dir)
     6.6  
     6.7 -      if (result1.ok)
     6.8 +      if (result1.ok) {
     6.9 +        for ((dir, pats) <- info.export_files) {
    6.10 +          Export.export_files(store, name, info.dir + dir,
    6.11 +            progress = if (verbose) progress else No_Progress,
    6.12 +            export_patterns = pats,
    6.13 +            export_prefix = name + ": ")
    6.14 +        }
    6.15          Present.finish(progress, store.browser_info, graph_file, info, name)
    6.16 +      }
    6.17  
    6.18        graph_file.delete
    6.19