# HG changeset patch # User wenzelm # Date 1510582023 -3600 # Node ID f11486d3158630349ae9ef9b6e6221f4dabb2c58 # Parent 46ce32fd5f53856219063911c890a2b5f8ba8ea2 init Mercurial repository for the generated session files; diff -r 46ce32fd5f53 -r f11486d31586 NEWS --- 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. diff -r 46ce32fd5f53 -r f11486d31586 src/Doc/System/Presentation.thy --- 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>\-T\ and \<^verbatim>\-A\ specify the document title and author explicitly, using {\LaTeX} source notation. + Option \<^verbatim>\-I\ initializes a Mercurial repository in the target directory, and + adds all generated files (without commit). + Option \<^verbatim>\-n\ specifies an alternative session name; otherwise the base name of the given directory is used. diff -r 46ce32fd5f53 -r f11486d31586 src/Pure/Tools/mkroot.scala --- 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) }) }