15 object Mercurial |
15 object Mercurial |
16 { |
16 { |
17 type Graph = isabelle.Graph[String, Unit] |
17 type Graph = isabelle.Graph[String, Unit] |
18 |
18 |
19 |
19 |
20 /* HTTP server addresses */ |
20 /* HTTP server */ |
21 |
21 |
22 object Address |
22 object Server |
23 { |
23 { |
24 def apply(root: String): Address = new Address(root) |
24 def apply(root: String): Server = new Server(root) |
25 } |
25 |
26 |
26 def start(root: Path): Server = |
27 final class Address private(val root: String) |
27 { |
|
28 val hg = repository(root) |
|
29 |
|
30 val server_process = Future.promise[Bash.Process] |
|
31 val server_root = Future.promise[String] |
|
32 Isabelle_Thread.fork("hg") { |
|
33 val process = |
|
34 Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) } |
|
35 server_process.fulfill_result(process) |
|
36 Exn.release(process).result(progress_stdout = |
|
37 line => if (!server_root.is_finished) { |
|
38 server_root.fulfill(Library.try_unsuffix("/", line).getOrElse(line)) |
|
39 }) |
|
40 } |
|
41 server_process.join |
|
42 |
|
43 new Server(server_root.join) { |
|
44 override def close(): Unit = server_process.join.terminate() |
|
45 } |
|
46 } |
|
47 } |
|
48 |
|
49 class Server private(val root: String) extends AutoCloseable |
28 { |
50 { |
29 override def toString: String = root |
51 override def toString: String = root |
|
52 |
|
53 def close(): Unit = () |
30 |
54 |
31 def changeset(rev: String = "tip", raw: Boolean = false): String = |
55 def changeset(rev: String = "tip", raw: Boolean = false): String = |
32 root + (if (raw) "/raw-rev/" else "/rev/") + rev |
56 root + (if (raw) "/raw-rev/" else "/rev/") + rev |
33 |
57 |
34 def file(path: Path, rev: String = "tip", raw: Boolean = false): String = |
58 def file(path: Path, rev: String = "tip", raw: Boolean = false): String = |
133 def clone_repository(source: String, root: Path, |
157 def clone_repository(source: String, root: Path, |
134 rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository = |
158 rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository = |
135 make_repository(root, "clone", |
159 make_repository(root, "clone", |
136 options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh) |
160 options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh) |
137 |
161 |
138 def setup_repository(address: Address, root: Path, ssh: SSH.System = SSH.Local): Repository = |
162 def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository = |
139 { |
163 { |
140 val source = address.root |
|
141 if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg } |
164 if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg } |
142 else clone_repository(source, root, options = "--noupdate", ssh = ssh) |
165 else clone_repository(source, root, options = "--noupdate", ssh = ssh) |
143 } |
166 } |
144 |
167 |
145 class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local) |
168 class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local) |
149 val root: Path = ssh.expand_path(root_path) |
172 val root: Path = ssh.expand_path(root_path) |
150 def root_url: String = ssh.hg_url + root.implode |
173 def root_url: String = ssh.hg_url + root.implode |
151 |
174 |
152 override def toString: String = ssh.hg_url + root.implode |
175 override def toString: String = ssh.hg_url + root.implode |
153 |
176 |
154 def command(name: String, args: String = "", options: String = "", |
177 def command_line(name: String, args: String = "", options: String = "", |
155 repository: Boolean = true): Process_Result = |
178 repository: Boolean = true): String = |
156 { |
179 { |
157 val cmdline = |
180 "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + |
158 "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + |
181 (if (repository) " --repository " + ssh.bash_path(root) else "") + |
159 (if (repository) " --repository " + ssh.bash_path(root) else "") + |
182 " --noninteractive " + name + " " + options + " " + args |
160 " --noninteractive " + name + " " + options + " " + args |
183 } |
161 ssh.execute(cmdline) |
184 |
|
185 def command( |
|
186 name: String, args: String = "", options: String = "", |
|
187 repository: Boolean = true): Process_Result = |
|
188 { |
|
189 ssh.execute(command_line(name, args = args, options = options, repository = repository)) |
162 } |
190 } |
163 |
191 |
164 def add(files: List[Path]): Unit = |
192 def add(files: List[Path]): Unit = |
165 hg.command("add", files.map(ssh.bash_path).mkString(" ")) |
193 hg.command("add", files.map(ssh.bash_path).mkString(" ")) |
166 |
194 |