--- a/src/Pure/General/mercurial.scala Sun May 29 11:43:13 2022 +0200
+++ b/src/Pure/General/mercurial.scala Sun May 29 11:45:32 2022 +0200
@@ -16,7 +16,8 @@
type Graph = isabelle.Graph[String, Unit]
- /* HTTP server */
+
+ /** HTTP server **/
object Server {
def apply(root: String): Server = new Server(root)
@@ -79,6 +80,9 @@
}
+
+ /** repository commands **/
+
/* command-line syntax */
def optional(s: String, prefix: String = ""): String =
@@ -258,7 +262,8 @@
}
- /* check files */
+
+ /** check files **/
def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) = {
val outside = new mutable.ListBuffer[Path]
@@ -285,7 +290,8 @@
}
- /* setup remote vs. local repository */
+
+ /** hg_setup **/
private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit = {
val hgrc = local_hg.root + Path.explode(".hg/hgrc")