init Mercurial repository for the generated session files;
authorwenzelm
Mon Nov 13 15:07:03 2017 +0100 (19 months ago)
changeset 67069f11486d31586
parent 67068 46ce32fd5f53
child 67070 85e6c1ff5be3
child 67072 b5c1f0c76d35
child 67076 fc877448602e
init Mercurial repository for the generated session files;
NEWS
src/Doc/System/Presentation.thy
src/Pure/Tools/mkroot.scala
     1.1 --- a/NEWS	Mon Nov 13 15:00:21 2017 +0100
     1.2 +++ b/NEWS	Mon Nov 13 15:07:03 2017 +0100
     1.3 @@ -104,6 +104,9 @@
     1.4  * The command-line tool "isabelle mkroot" now always produces a document
     1.5  outline: its options have been adapted accordingly. INCOMPATIBILITY.
     1.6  
     1.7 +* The command-line tool "isabelle mkroot -I" initializes a Mercurial
     1.8 +repository for the generated session files.
     1.9 +
    1.10  * Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
    1.11  support has been discontinued.
    1.12  
     2.1 --- a/src/Doc/System/Presentation.thy	Mon Nov 13 15:00:21 2017 +0100
     2.2 +++ b/src/Doc/System/Presentation.thy	Mon Nov 13 15:07:03 2017 +0100
     2.3 @@ -98,6 +98,7 @@
     2.4  
     2.5    Options are:
     2.6      -A LATEX     provide author in LaTeX notation (default: user name)
     2.7 +    -I           init Mercurial repository and add generated files
     2.8      -T LATEX     provide title in LaTeX notation (default: session name)
     2.9      -n NAME      alternative session name (default: directory base name)
    2.10  
    2.11 @@ -116,6 +117,9 @@
    2.12    Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly,
    2.13    using {\LaTeX} source notation.
    2.14  
    2.15 +  Option \<^verbatim>\<open>-I\<close> initializes a Mercurial repository in the target directory, and
    2.16 +  adds all generated files (without commit).
    2.17 +
    2.18    Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name
    2.19    of the given directory is used.
    2.20  
     3.1 --- a/src/Pure/Tools/mkroot.scala	Mon Nov 13 15:00:21 2017 +0100
     3.2 +++ b/src/Pure/Tools/mkroot.scala	Mon Nov 13 15:07:03 2017 +0100
     3.3 @@ -22,6 +22,7 @@
     3.4      session_name: String = "",
     3.5      session_dir: Path = Path.current,
     3.6      session_parent: String = "",
     3.7 +    init_repos: Boolean = false,
     3.8      title: String = "",
     3.9      author: String = "",
    3.10      progress: Progress = No_Progress)
    3.11 @@ -37,6 +38,9 @@
    3.12      val document_path = session_dir + Path.explode("document")
    3.13      if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
    3.14  
    3.15 +    val root_tex = session_dir + Path.explode("document/root.tex")
    3.16 +
    3.17 +
    3.18      progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
    3.19  
    3.20  
    3.21 @@ -61,7 +65,6 @@
    3.22      /* document directory */
    3.23  
    3.24      {
    3.25 -      val root_tex = session_dir + Path.explode("document/root.tex")
    3.26        progress.echo("  creating " + root_tex)
    3.27  
    3.28        Isabelle_System.mkdirs(root_tex.dir)
    3.29 @@ -130,6 +133,33 @@
    3.30      }
    3.31  
    3.32  
    3.33 +    /* Mercurial repository */
    3.34 +
    3.35 +    if (init_repos) {
    3.36 +      progress.echo("  \nInitializing Mercurial repository " + session_dir)
    3.37 +
    3.38 +      val hg = Mercurial.init_repository(session_dir)
    3.39 +
    3.40 +      val hg_ignore = session_dir + Path.explode(".hgignore")
    3.41 +      File.write(hg_ignore,
    3.42 +"""syntax: glob
    3.43 +
    3.44 +*~
    3.45 +*.marks
    3.46 +*.orig
    3.47 +*.rej
    3.48 +.DS_Store
    3.49 +.swp
    3.50 +
    3.51 +syntax: regexp
    3.52 +
    3.53 +^output/
    3.54 +""")
    3.55 +
    3.56 +      hg.add(List(root_path, root_tex, hg_ignore))
    3.57 +    }
    3.58 +
    3.59 +
    3.60      /* notes */
    3.61  
    3.62      {
    3.63 @@ -149,6 +179,7 @@
    3.64    val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
    3.65    {
    3.66      var author = ""
    3.67 +    var init_repos = false
    3.68      var title = ""
    3.69      var session_name = ""
    3.70  
    3.71 @@ -157,12 +188,14 @@
    3.72  
    3.73    Options are:
    3.74      -A LATEX     provide author in LaTeX notation (default: user name)
    3.75 +    -I           init Mercurial repository and add generated files
    3.76      -T LATEX     provide title in LaTeX notation (default: session name)
    3.77      -n NAME      alternative session name (default: directory base name)
    3.78  
    3.79    Prepare session root directory (default: current directory).
    3.80  """,
    3.81        "A:" -> (arg => author = arg),
    3.82 +      "I" -> (arg => init_repos = true),
    3.83        "T:" -> (arg => title = arg),
    3.84        "n:" -> (arg => session_name = arg))
    3.85  
    3.86 @@ -175,7 +208,7 @@
    3.87          case _ => getopts.usage()
    3.88        }
    3.89  
    3.90 -    mkroot(session_name = session_name, session_dir = session_dir, author = author, title = title,
    3.91 -      progress = new Console_Progress)
    3.92 +    mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
    3.93 +      author = author, title = title, progress = new Console_Progress)
    3.94    })
    3.95  }