init Mercurial repository for the generated session files;
authorwenzelm
Mon, 13 Nov 2017 15:07:03 +0100
changeset 67069 f11486d31586
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
--- a/NEWS	Mon Nov 13 15:00:21 2017 +0100
+++ b/NEWS	Mon Nov 13 15:07:03 2017 +0100
@@ -104,6 +104,9 @@
 * The command-line tool "isabelle mkroot" now always produces a document
 outline: its options have been adapted accordingly. INCOMPATIBILITY.
 
+* The command-line tool "isabelle mkroot -I" initializes a Mercurial
+repository for the generated session files.
+
 * Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
 support has been discontinued.
 
--- a/src/Doc/System/Presentation.thy	Mon Nov 13 15:00:21 2017 +0100
+++ b/src/Doc/System/Presentation.thy	Mon Nov 13 15:07:03 2017 +0100
@@ -98,6 +98,7 @@
 
   Options are:
     -A LATEX     provide author in LaTeX notation (default: user name)
+    -I           init Mercurial repository and add generated files
     -T LATEX     provide title in LaTeX notation (default: session name)
     -n NAME      alternative session name (default: directory base name)
 
@@ -116,6 +117,9 @@
   Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly,
   using {\LaTeX} source notation.
 
+  Option \<^verbatim>\<open>-I\<close> initializes a Mercurial repository in the target directory, and
+  adds all generated files (without commit).
+
   Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name
   of the given directory is used.
 
--- a/src/Pure/Tools/mkroot.scala	Mon Nov 13 15:00:21 2017 +0100
+++ b/src/Pure/Tools/mkroot.scala	Mon Nov 13 15:07:03 2017 +0100
@@ -22,6 +22,7 @@
     session_name: String = "",
     session_dir: Path = Path.current,
     session_parent: String = "",
+    init_repos: Boolean = false,
     title: String = "",
     author: String = "",
     progress: Progress = No_Progress)
@@ -37,6 +38,9 @@
     val document_path = session_dir + Path.explode("document")
     if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
 
+    val root_tex = session_dir + Path.explode("document/root.tex")
+
+
     progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
 
 
@@ -61,7 +65,6 @@
     /* document directory */
 
     {
-      val root_tex = session_dir + Path.explode("document/root.tex")
       progress.echo("  creating " + root_tex)
 
       Isabelle_System.mkdirs(root_tex.dir)
@@ -130,6 +133,33 @@
     }
 
 
+    /* Mercurial repository */
+
+    if (init_repos) {
+      progress.echo("  \nInitializing Mercurial repository " + session_dir)
+
+      val hg = Mercurial.init_repository(session_dir)
+
+      val hg_ignore = session_dir + Path.explode(".hgignore")
+      File.write(hg_ignore,
+"""syntax: glob
+
+*~
+*.marks
+*.orig
+*.rej
+.DS_Store
+.swp
+
+syntax: regexp
+
+^output/
+""")
+
+      hg.add(List(root_path, root_tex, hg_ignore))
+    }
+
+
     /* notes */
 
     {
@@ -149,6 +179,7 @@
   val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
   {
     var author = ""
+    var init_repos = false
     var title = ""
     var session_name = ""
 
@@ -157,12 +188,14 @@
 
   Options are:
     -A LATEX     provide author in LaTeX notation (default: user name)
+    -I           init Mercurial repository and add generated files
     -T LATEX     provide title in LaTeX notation (default: session name)
     -n NAME      alternative session name (default: directory base name)
 
   Prepare session root directory (default: current directory).
 """,
       "A:" -> (arg => author = arg),
+      "I" -> (arg => init_repos = true),
       "T:" -> (arg => title = arg),
       "n:" -> (arg => session_name = arg))
 
@@ -175,7 +208,7 @@
         case _ => getopts.usage()
       }
 
-    mkroot(session_name = session_name, session_dir = session_dir, author = author, title = title,
-      progress = new Console_Progress)
+    mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
+      author = author, title = title, progress = new Console_Progress)
   })
 }