# HG changeset patch
# User wenzelm
# Date 1653817532 -7200
# Node ID ff6d4b48f23b20f747138cea1345e201249ad355
# Parent  63f904ae4134d4bbafe64be0b103264dcebaed20
tuned comments;

diff -r 63f904ae4134 -r ff6d4b48f23b src/Pure/General/mercurial.scala
--- 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")