diff --git a/src/Pure/General/file.scala b/src/Pure/General/file.scala --- a/src/Pure/General/file.scala +++ b/src/Pure/General/file.scala @@ -1,358 +1,358 @@ /* Title: Pure/General/file.scala Author: Makarius File-system operations. */ package isabelle import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader, File => JFile, IOException} import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath, Files, SimpleFileVisitor, FileVisitOption, FileVisitResult, FileSystemException} import java.nio.file.attribute.BasicFileAttributes import java.net.{URL, MalformedURLException} import java.util.zip.{GZIPInputStream, GZIPOutputStream} import java.util.regex.Pattern import java.util.EnumSet import org.tukaani.xz.{XZInputStream, XZOutputStream} import scala.collection.mutable import scala.util.matching.Regex object File { /* standard path (Cygwin or Posix) */ def standard_path(path: Path): String = path.expand.implode def standard_path(platform_path: String): String = if (Platform.is_windows) { val Platform_Root = new Regex("(?i)" + Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""") val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") platform_path.replace('/', '\\') match { case Platform_Root(rest) => "/" + rest.replace('\\', '/') case Drive(letter, rest) => "/cygdrive/" + Word.lowercase(letter) + (if (rest == "") "" else "/" + rest.replace('\\', '/')) case path => path.replace('\\', '/') } } else platform_path def standard_path(file: JFile): String = standard_path(file.getPath) def standard_url(name: String): String = try { val url = new URL(name) if (url.getProtocol == "file" && Url.is_wellformed_file(name)) standard_path(Url.parse_file(name)) else name } catch { case _: MalformedURLException => standard_path(name) } /* platform path (Windows or Posix) */ private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") private val Named_Root = new Regex("//+([^/]*)(.*)") def platform_path(standard_path: String): String = if (Platform.is_windows) { val result_path = new StringBuilder val rest = standard_path match { case Cygdrive(drive, rest) => result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) rest case Named_Root(root, rest) => result_path ++= JFile.separator result_path ++= JFile.separator result_path ++= root rest case path if path.startsWith("/") => result_path ++= Isabelle_System.cygwin_root() path case path => path } for (p <- space_explode('/', rest) if p != "") { val len = result_path.length if (len > 0 && result_path(len - 1) != JFile.separatorChar) result_path += JFile.separatorChar result_path ++= p } result_path.toString } else standard_path def platform_path(path: Path): String = platform_path(standard_path(path)) def platform_file(path: Path): JFile = new JFile(platform_path(path)) /* platform files */ def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile def absolute_name(file: JFile): String = absolute(file).getPath def canonical(file: JFile): JFile = file.getCanonicalFile def canonical_name(file: JFile): String = canonical(file).getPath def path(file: JFile): Path = Path.explode(standard_path(file)) def pwd(): Path = path(Path.current.absolute_file) /* relative paths */ def relative_path(base: Path, other: Path): Option[Path] = { val base_path = base.file.toPath val other_path = other.file.toPath if (other_path.startsWith(base_path)) Some(path(base_path.relativize(other_path).toFile)) else None } def rebase_path(base: Path, other: Path): Option[Path] = relative_path(base, other).map(base + _) /* bash path */ def bash_path(path: Path): String = Bash.string(standard_path(path)) def bash_path(file: JFile): String = Bash.string(standard_path(file)) /* directory entries */ def check_dir(path: Path): Path = if (path.is_dir) path else error("No such directory: " + path) def check_file(path: Path): Path = if (path.is_file) path else error("No such file: " + path) /* directory content */ def read_dir(dir: Path): List[String] = { if (!dir.is_dir) error("No such directory: " + dir.toString) val files = dir.file.listFiles if (files == null) Nil else files.toList.map(_.getName).sorted } def find_files( start: JFile, pred: JFile => Boolean = _ => true, include_dirs: Boolean = false, follow_links: Boolean = false): List[JFile] = { val result = new mutable.ListBuffer[JFile] def check(file: JFile) { if (pred(file)) result += file } if (start.isFile) check(start) else if (start.isDirectory) { val options = if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS) else EnumSet.noneOf(classOf[FileVisitOption]) Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE, new SimpleFileVisitor[JPath] { override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult = { if (include_dirs) check(path.toFile) FileVisitResult.CONTINUE } override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult = { val file = path.toFile if (include_dirs || !file.isDirectory) check(file) FileVisitResult.CONTINUE } } ) } result.toList } /* read */ def read(file: JFile): String = Bytes.read(file).text def read(path: Path): String = read(path.file) def read_stream(reader: BufferedReader): String = { val output = new StringBuilder(100) var c = -1 while ({ c = reader.read; c != -1 }) output += c.toChar reader.close output.toString } def read_stream(stream: InputStream): String = read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) def read_gzip(file: JFile): String = read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_gzip(path: Path): String = read_gzip(path.file) def read_xz(file: JFile): String = read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_xz(path: Path): String = read_xz(path.file) /* read lines */ def read_line(reader: BufferedReader): Option[String] = { val line = try { reader.readLine} catch { case _: IOException => null } if (line == null) None else Some(line) } def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = { val result = new mutable.ListBuffer[String] var line: Option[String] = None while ({ line = read_line(reader); line.isDefined }) { progress(line.get) result += line.get } reader.close result.toList } /* write */ def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream) { val stream = make_stream(new FileOutputStream(file)) using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text)) } def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s) def write(path: Path, text: CharSequence): Unit = write(path.file, text) def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text) def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit = File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options)) def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options()) def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit = write_xz(path.file, text, options) def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options()) def write_backup(path: Path, text: CharSequence) { if (path.is_file) move(path, path.backup) write(path, text) } def write_backup2(path: Path, text: CharSequence) { if (path.is_file) move(path, path.backup2) write(path, text) } /* append */ def append(file: JFile, text: CharSequence): Unit = Files.write(file.toPath, UTF8.bytes(text.toString), StandardOpenOption.APPEND, StandardOpenOption.CREATE) def append(path: Path, text: CharSequence): Unit = append(path.file, text) /* eq */ def eq(file1: JFile, file2: JFile): Boolean = try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) } catch { case ERROR(_) => false } def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) /* eq_content */ def eq_content(file1: JFile, file2: JFile): Boolean = if (eq(file1, file2)) true else if (file1.length != file2.length) false else Bytes.read(file1) == Bytes.read(file2) def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file) /* copy */ def copy(src: JFile, dst: JFile) { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!eq(src, target)) Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) /* move */ def move(src: JFile, dst: JFile) { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file) /* symbolic link */ def link(src: Path, dst: Path, force: Boolean = false) { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => Cygwin.link(standard_path(src), target) case _: FileSystemException if Platform.is_windows => Cygwin.link(standard_path(src), target) } } /* permissions */ def is_executable(path: Path): Boolean = { if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok else path.file.canExecute } def set_executable(path: Path, flag: Boolean) { - if (Platform.is_windows && flag) Isabelle_System.bash("chmod a+x " + bash_path(path)).check - else if (Platform.is_windows) Isabelle_System.bash("chmod a-x " + bash_path(path)).check + if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path) + else if (Platform.is_windows) Isabelle_System.chmod("a-x", path) else path.file.setExecutable(flag, false) } } diff --git a/src/Pure/ML/ml_process.scala b/src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala +++ b/src/Pure/ML/ml_process.scala @@ -1,189 +1,189 @@ /* Title: Pure/ML/ml_process.scala Author: Makarius The raw ML process. */ package isabelle import java.io.{File => JFile} object ML_Process { def apply(options: Options, logic: String = "", args: List[String] = Nil, dirs: List[Path] = Nil, modes: List[String] = Nil, raw_ml_system: Boolean = false, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => (), sessions_structure: Option[Sessions.Structure] = None, session_base: Option[Sessions.Base] = None, store: Option[Sessions.Store] = None): Bash.Process = { val logic_name = Isabelle_System.default_logic(logic) val _store = store.getOrElse(Sessions.store(options)) val sessions_structure1 = sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs)) val heaps: List[String] = if (raw_ml_system) Nil else { sessions_structure1.selection(Sessions.Selection.session(logic_name)). build_requirements(List(logic_name)). map(a => File.platform_path(_store.the_heap(a))) } val eval_init = if (heaps.isEmpty) { List( """ fun chapter (_: string) = (); fun section (_: string) = (); fun subsection (_: string) = (); fun subsubsection (_: string) = (); fun paragraph (_: string) = (); fun subparagraph (_: string) = (); val ML_file = PolyML.use; """, if (Platform.is_windows) "fun exit 0 = OS.Process.exit OS.Process.success" + " | exit 1 = OS.Process.exit OS.Process.failure" + " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" else "fun exit rc = Posix.Process.exit (Word8.fromInt rc)", "PolyML.Compiler.prompt1 := \"Poly/ML> \"", "PolyML.Compiler.prompt2 := \"Poly/ML# \"") } else List( "(PolyML.SaveState.loadHierarchy " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + ML_Syntax.print_string_bytes(": " + logic_name + "\n") + "); OS.Process.exit OS.Process.failure)") val eval_modes = if (modes.isEmpty) Nil else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes)) // options val isabelle_process_options = Isabelle_System.tmp_file("options") - Isabelle_System.bash("chmod 600 " + File.bash_path(File.path(isabelle_process_options))).check + Isabelle_System.chmod("600", File.path(isabelle_process_options)) File.write(isabelle_process_options, YXML.string_of_body(options.encode)) val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") // session base val eval_session_base = session_base match { case None => Nil case Some(base) => def print_table(table: List[(String, String)]): String = ML_Syntax.print_list( ML_Syntax.print_pair( ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table) def print_list(list: List[String]): String = ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list) def print_sessions(list: List[(String, Position.T)]): String = ML_Syntax.print_list( ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list) List("Resources.init_session_base" + " {session_positions = " + print_sessions(sessions_structure1.session_positions) + ", session_directories = " + print_table(sessions_structure1.dest_session_directories) + ", docs = " + print_list(base.doc_names) + ", global_theories = " + print_table(base.global_theories.toList) + ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}") } // process val eval_process = if (heaps.isEmpty) List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))) else List("Isabelle_Process.init ()") // ISABELLE_TMP val isabelle_tmp = Isabelle_System.tmp_dir("process") val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) val ml_runtime_options = { val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) val ml_options1 = if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options else ml_options ::: List("--gcthreads", options.int("threads").toString) val ml_options2 = if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1 else ml_options1 ::: List("--codepage", "utf8") ml_options2 } // bash val bash_args = ml_runtime_options ::: (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process). map(eval => List("--eval", eval)).flatten ::: args Bash.process( "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + Bash.strings(bash_args), cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect, cleanup = () => { isabelle_process_options.delete Isabelle_System.rm_tree(isabelle_tmp) cleanup() }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => { var dirs: List[Path] = Nil var eval_args: List[String] = Nil var logic = Isabelle_System.getenv("ISABELLE_LOGIC") var modes: List[String] = Nil var options = Options.init() val getopts = Getopts(""" Usage: isabelle process [OPTIONS] Options are: -T THEORY load theory -d DIR include session directory -e ML_EXPR evaluate ML expression on startup -f ML_FILE evaluate ML file on startup -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) -m MODE add print mode for output -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) Run the raw Isabelle ML process in batch mode. """, "T:" -> (arg => eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), "o:" -> (arg => options = options + arg)) val more_args = getopts(args) if (args.isEmpty || !more_args.isEmpty) getopts.usage() val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes). result().print_stdout.rc sys.exit(rc) }) } diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,385 +1,394 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Fundamental Isabelle system environment: quasi-static module with optional init operation. */ package isabelle import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult} import java.nio.file.attribute.BasicFileAttributes import scala.collection.mutable object Isabelle_System { /** bootstrap information **/ def jdk_home(): String = { val java_home = System.getProperty("java.home", "") val home = new JFile(java_home) val parent = home.getParent if (home.getName == "jre" && parent != null && (new JFile(new JFile(parent, "bin"), "javac")).exists) parent else java_home } def bootstrap_directory( preference: String, envar: String, property: String, description: String): String = { val value = proper_string(preference) orElse // explicit argument proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process error("Unknown " + description + " directory") if ((new JFile(value)).isDirectory) value else error("Bad " + description + " directory " + quote(value)) } /** implicit settings environment **/ @volatile private var _settings: Option[Map[String, String]] = None def settings(): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check _settings.get } def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized { if (_settings.isEmpty) { import scala.collection.JavaConversions._ val isabelle_root1 = bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") val cygwin_root1 = if (Platform.is_windows) bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") else "" if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) def set_cygwin_root() { if (Platform.is_windows) _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) } set_cygwin_root() def default(env: Map[String, String], entry: (String, String)): Map[String, String] = if (env.isDefinedAt(entry._1) || entry._2 == "") env else env + entry val env = { val temp_windows = { val temp = if (Platform.is_windows) System.getenv("TEMP") else null if (temp != null && temp.contains('\\')) temp else "" } val user_home = System.getProperty("user.home", "") val isabelle_app = System.getProperty("isabelle.app", "") default( default( default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), "TEMP_WINDOWS" -> temp_windows), "HOME" -> user_home), "ISABELLE_APP" -> "true") } val settings = { val dump = JFile.createTempFile("settings", null) dump.deleteOnExit try { val cmd1 = if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l", File.standard_path(isabelle_root1 + "\\bin\\isabelle")) else List(isabelle_root1 + "/bin/isabelle") val cmd = cmd1 ::: List("getenv", "-d", dump.toString) val (output, rc) = process_output(process(cmd, env = env, redirect = true)) if (rc != 0) error(output) val entries = (for (entry <- File.read(dump).split("\u0000") if entry != "") yield { val i = entry.indexOf('=') if (i <= 0) entry -> "" else entry.substring(0, i) -> entry.substring(i + 1) }).toMap entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } finally { dump.delete } } _settings = Some(settings) set_cygwin_root() } } /* getenv */ def getenv(name: String, env: Map[String, String] = settings()): String = env.getOrElse(name, "") def getenv_strict(name: String, env: Map[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") def isabelle_id(): String = proper_string(getenv("ISABELLE_ID")) getOrElse Mercurial.repository(Path.explode("~~")).parent() /** file-system operations **/ + /* permissions */ + + def chmod(arg: String, path: Path): Unit = + bash("chmod " + Bash.string(arg) + " -- " + File.bash_path(path)).check + + def chown(arg: String, path: Path): Unit = + bash("chown " + Bash.string(arg) + " -- " + File.bash_path(path)).check + + /* directories */ def mkdirs(path: Path): Unit = if (!path.is_dir) { bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"") if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path))) } def copy_dir(dir1: Path, dir2: Path): Unit = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check /* tmp files */ private def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: Path): Unit = rm_tree(root.file) def rm_tree(root: JFile) { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit) { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) File.move(dir, old_dir) File.move(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* raw process */ def process(command_line: List[String], cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false): Process = { val proc = new ProcessBuilder proc.command(command_line:_*) // fragile on Windows if (cwd != null) proc.directory(cwd) if (env != null) { proc.environment.clear for ((x, y) <- env) proc.environment.put(x, y) } proc.redirectErrorStream(redirect) proc.start } def process_output(proc: Process): (String, Int) = { proc.getOutputStream.close val output = File.read_stream(proc.getInputStream) val rc = try { proc.waitFor } finally { proc.getInputStream.close proc.getErrorStream.close proc.destroy Thread.interrupted } (output, rc) } def kill(signal: String, group_pid: String): (String, Int) = { val bash = if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe") else List("/usr/bin/env", "bash") process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) } /* GNU bash */ def bash(script: String, cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), progress_limit: Option[Long] = None, strict: Boolean = true, cleanup: () => Unit = () => ()): Process_Result = { Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(progress_stdout, progress_stderr, progress_limit, strict) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, redirect: Boolean = false): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* components */ def components(): List[Path] = Path.split(getenv_strict("ISABELLE_COMPONENTS")) /* classes */ def init_classes[A](variable: String): List[A] = { for (name <- space_explode(':', Isabelle_System.getenv_strict(variable))) yield { def err(msg: String): Nothing = error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) try { Class.forName(name).asInstanceOf[Class[A]].newInstance() } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } } /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC") } } } diff --git a/src/Pure/System/linux.scala b/src/Pure/System/linux.scala --- a/src/Pure/System/linux.scala +++ b/src/Pure/System/linux.scala @@ -1,141 +1,141 @@ /* Title: Pure/System/linux.scala Author: Makarius Specific support for Linux, notably Ubuntu/Debian. */ package isabelle import scala.util.matching.Regex object Linux { /* check system */ def check_system(): Unit = if (!Platform.is_linux) error("Not a Linux system") def check_system_root(): Unit = { check_system() if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)") } /* release */ object Release { private val ID = """^Distributor ID:\s*(\S.*)$""".r private val RELEASE = """^Release:\s*(\S.*)$""".r private val DESCRIPTION = """^Description:\s*(\S.*)$""".r def apply(): Release = { val lines = Isabelle_System.bash("lsb_release -a").check.out_lines def find(R: Regex): String = lines.collectFirst({ case R(a) => a }).getOrElse("Unknown") new Release(find(ID), find(RELEASE), find(DESCRIPTION)) } } final class Release private(val id: String, val release: String, val description: String) { override def toString: String = description def is_ubuntu: Boolean = id == "Ubuntu" } /* packages */ def reboot_required(): Boolean = Path.explode("/var/run/reboot-required").is_file def check_reboot_required(): Unit = if (reboot_required()) error("Reboot required") def package_update(progress: Progress = No_Progress): Unit = progress.bash( """apt-get update -y && apt-get upgrade -y && apt autoremove -y""", echo = true).check def package_install(packages: List[String], progress: Progress = No_Progress): Unit = progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check /* users */ def user_exists(name: String): Boolean = Isabelle_System.bash("id " + Bash.string(name)).ok def user_entry(name: String, field: Int): String = { val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check val fields = space_explode(':', result.out) if (1 <= field && field <= fields.length) fields(field - 1) else error("No passwd field " + field + " for user " + quote(name)) } def user_description(name: String): String = user_entry(name, 5).takeWhile(_ != ',') def user_home(name: String): String = user_entry(name, 6) def user_add(name: String, description: String = "", system: Boolean = false, ssh_setup: Boolean = false) { require(!description.contains(',')) if (user_exists(name)) error("User already exists: " + quote(name)) Isabelle_System.bash( "adduser --quiet --disabled-password --gecos " + Bash.string(description) + (if (system) " --system --group --shell /bin/bash " else "") + " " + Bash.string(name)).check if (ssh_setup) { val id_rsa = user_home(name) + "/.ssh/id_rsa" Isabelle_System.bash(""" if [ ! -f """ + Bash.string(id_rsa) + """ ] then yes '\n' | sudo -i -u """ + Bash.string(name) + """ ssh-keygen -q -f """ + Bash.string(id_rsa) + """ fi """).check } } /* system services */ def service_operation(op: String, name: String): Unit = Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check def service_enable(name: String) { service_operation("enable", name) } def service_disable(name: String) { service_operation("disable", name) } def service_start(name: String) { service_operation("start", name) } def service_stop(name: String) { service_operation("stop", name) } def service_restart(name: String) { service_operation("restart", name) } def service_shutdown(name: String) { try { service_stop(name) } catch { case ERROR(_) => } } def service_install(name: String, spec: String) { service_shutdown(name) val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service") File.write(service_file, spec) - Isabelle_System.bash("chmod 0644 " + File.bash_path(service_file)).check + Isabelle_System.chmod("0644", service_file) service_enable(name) service_restart(name) } } diff --git a/src/Pure/Thy/present.scala b/src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala +++ b/src/Pure/Thy/present.scala @@ -1,323 +1,323 @@ /* Title: Pure/Thy/present.scala Author: Makarius Theory presentation: HTML. */ package isabelle import java.io.{File => JFile} import scala.collection.immutable.SortedMap object Present { /* maintain chapter index -- NOT thread-safe */ private val sessions_path = Path.basic(".sessions") private def read_sessions(dir: Path): List[(String, String)] = { val path = dir + sessions_path if (path.is_file) { import XML.Decode._ list(pair(string, string))(Symbol.decode_yxml(File.read(path))) } else Nil } private def write_sessions(dir: Path, sessions: List[(String, String)]) { import XML.Encode._ File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) } def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)]) { val dir = browser_info + Path.basic(chapter) Isabelle_System.mkdirs(dir) val sessions0 = try { read_sessions(dir) } catch { case _: XML.Error => Nil } val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList write_sessions(dir, sessions) val title = "Isabelle/" + chapter + " sessions" HTML.write_document(dir, "index.html", List(HTML.title(title + " (" + Distribution.version + ")")), HTML.chapter(title) :: (if (sessions.isEmpty) Nil else List(HTML.div("sessions", List(HTML.description( sessions.map({ case (name, description) => val descr = Symbol.trim_blank_lines(description) (List(HTML.link(name + "/index.html", HTML.text(name))), if (descr == "") Nil else HTML.break ::: List(HTML.pre(HTML.text(descr)))) }))))))) } def make_global_index(browser_info: Path) { if (!(browser_info + Path.explode("index.html")).is_file) { Isabelle_System.mkdirs(browser_info) File.copy(Path.explode("~~/lib/logo/isabelle.gif"), browser_info + Path.explode("isabelle.gif")) File.write(browser_info + Path.explode("index.html"), File.read(Path.explode("~~/lib/html/library_index_header.template")) + File.read(Path.explode("~~/lib/html/library_index_content.template")) + File.read(Path.explode("~~/lib/html/library_index_footer.template"))) } } /* finish session */ def finish( progress: Progress, browser_info: Path, graph_file: JFile, info: Sessions.Info, name: String) { val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name) val session_fonts = session_prefix + Path.explode("fonts") if (info.options.bool("browser_info")) { Isabelle_System.mkdirs(session_fonts) val session_graph = session_prefix + Path.basic("session_graph.pdf") File.copy(graph_file, session_graph.file) - Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph)) + Isabelle_System.chmod("a+r", session_graph) HTML.write_isabelle_css(session_prefix) for (entry <- Isabelle_Fonts.fonts(hidden = true)) File.copy(entry.path, session_fonts) } } /** preview **/ sealed case class Preview(title: String, content: String) def preview( resources: Resources, snapshot: Document.Snapshot, plain_text: Boolean = false, fonts_url: String => String = HTML.fonts_url()): Preview = { require(!snapshot.is_outdated) def output_document(title: String, body: XML.Body): String = HTML.output_document( List( HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)), HTML.title(title)), List(HTML.source(body)), css = "", structural = false) val name = snapshot.node_name if (plain_text) { val title = "File " + quote(name.path.file_name) val content = output_document(title, HTML.text(snapshot.node.source)) Preview(title, content) } else { resources.make_preview(snapshot) match { case Some(preview) => preview case None => val title = if (name.is_theory) "Theory " + quote(name.theory_base_name) else "File " + quote(name.path.file_name) val content = output_document(title, pide_document(snapshot)) Preview(title, content) } } } /* PIDE document */ private val document_elements = Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements + Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE private val div_elements = Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, HTML.descr.name) private def html_div(html: XML.Body): Boolean = html exists { case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) case XML.Text(_) => false } private def html_class(c: String, html: XML.Body): XML.Tree = if (html.forall(_ == HTML.no_text)) HTML.no_text else if (html_div(html)) HTML.div(c, html) else HTML.span(c, html) private def make_html(xml: XML.Body): XML.Body = xml map { case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) => html_class(Markup.Language.DOCUMENT, make_html(body)) case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body)) case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body)) case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text case XML.Elem(Markup.Markdown_List(kind), body) => if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body)) case XML.Elem(markup, body) => val name = markup.name val html = markup.properties match { case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => List(html_class(kind, make_html(body))) case _ => make_html(body) } Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { case Some(c) => html_class(c.toString, html) case None => html_class(name, html) } case XML.Text(text) => XML.Text(Symbol.decode(text)) } def pide_document(snapshot: Document.Snapshot): XML.Body = make_html(snapshot.markup_to_XML(Text.Range.full, document_elements)) /** build document **/ val default_document_name = "document" val default_document_format = "pdf" val document_formats = List("pdf", "dvi") def default_document_dir(name: String): Path = Path.explode("output") + Path.basic(name) def document_tags(tags: List[String]): String = { cat_lines( tags.map(tag => tag.toList match { case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" case cs => "\\isakeeptag{" + cs.mkString + "}" })) + "\n" } def build_document( document_name: String = default_document_name, document_format: String = default_document_format, document_dir: Option[Path] = None, tags: List[String] = Nil) { val document_target = Path.parent + Path.explode(document_name).ext(document_format) if (!document_formats.contains(document_format)) error("Bad document output format: " + quote(document_format)) val dir = document_dir getOrElse default_document_dir(document_name) if (!dir.is_dir) error("Bad document output directory " + dir) val root_name = { val root1 = "root_" + document_name if ((dir + Path.explode(root1).ext("tex")).is_file) root1 else "root" } /* bash scripts */ def root_bash(ext: String): String = Bash.string(root_name + "." + ext) def latex_bash(fmt: String, ext: String = "tex"): String = "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext) def bash(script: String): Process_Result = Isabelle_System.bash(script, cwd = dir.file) /* prepare document */ File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags)) List("log", "blg").foreach(ext => (dir + Path.explode(root_name).ext(ext)).file.delete) val result = if ((dir + Path.explode("build")).is_file) { bash("./build " + Bash.string(document_format) + " " + Bash.string(document_name)) } else { bash( List( latex_bash("sty"), latex_bash(document_format), "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", latex_bash(document_format), latex_bash(document_format)).mkString(" && ")) } /* result */ if (!result.ok) { cat_error( Library.trim_line(result.err), cat_lines(Latex.latex_errors(dir, root_name) ::: Bibtex.bibtex_errors(dir, root_name)), "Failed to build document in " + File.path(dir.absolute_file)) } bash("if [ -f " + root_bash(document_format) + " ]; then cp -f " + root_bash(document_format) + " " + File.bash_path(document_target) + "; fi").check } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("document", "prepare theory session document", args => { var document_dir: Option[Path] = None var document_name = default_document_name var document_format = default_document_format var tags: List[String] = Nil val getopts = Getopts(""" Usage: isabelle document [OPTIONS] Options are: -d DIR document output directory (default """ + default_document_dir(default_document_name) + """) -n NAME document name (default """ + quote(default_document_name) + """) -o FORMAT document format: """ + commas(document_formats.map(fmt => fmt + (if (fmt == default_document_format) " (default)" else ""))) + """ -t TAGS markup for tagged regions Prepare the theory session document in document directory, producing the specified output format. """, "d:" -> (arg => document_dir = Some(Path.explode(arg))), "n:" -> (arg => document_name = arg), "o:" -> (arg => document_format = arg), "t:" -> (arg => tags = space_explode(',', arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() try { build_document(document_dir = document_dir, document_name = document_name, document_format = document_format, tags = tags) } catch { case ERROR(msg) => Output.writeln(msg); sys.exit(2) } }) } diff --git a/src/Pure/Tools/phabricator.scala b/src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala +++ b/src/Pure/Tools/phabricator.scala @@ -1,701 +1,698 @@ /* Title: Pure/Tools/phabricator.scala Author: Makarius Support for Phabricator server, notably for Ubuntu 18.04 LTS. See also: - https://www.phacility.com/phabricator - https://secure.phabricator.com/book/phabricator */ package isabelle import scala.util.matching.Regex object Phabricator { /** defaults **/ /* required packages */ val packages: List[String] = Build_Docker.packages ::: List( // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61 "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring", // more packages "php-zip", "python-pygments", "ssh") /* global system resources */ val www_user = "www-data" val daemon_user = "phabricator" val sshd_config = Path.explode("/etc/ssh/sshd_config") /* installation parameters */ val default_name = "vcs" def phabricator_name(name: String = "", ext: String = ""): String = "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext) def isabelle_phabricator_name(name: String = "", ext: String = ""): String = "isabelle-" + phabricator_name(name = name, ext = ext) def default_root(name: String): Path = Path.explode("/var/www") + Path.basic(phabricator_name(name = name)) def default_repo(name: String): Path = default_root(name) + Path.basic("repo") val default_mailers: Path = Path.explode("mailers.json") val default_system_port = 22 val alternative_system_port = 222 val default_server_port = 2222 /** global configuration **/ val global_config = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf")) sealed case class Config(name: String, root: Path) { def home: Path = root + Path.explode(phabricator_name()) def execute(command: String): Process_Result = Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check } def read_config(): List[Config] = { if (global_config.is_file) { for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty) yield { space_explode(':', entry) match { case List(name, root) => Config(name, Path.explode(root)) case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry)) } } } else Nil } def write_config(configs: List[Config]) { File.write(global_config, configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n")) } def get_config(name: String): Config = read_config().find(config => config.name == name) getOrElse error("Bad Isabelle/Phabricator installation " + quote(name)) /** command-line tools **/ /* Isabelle tool wrapper */ val isabelle_tool1 = Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", args => { var list = false var name = default_name val getopts = Getopts(""" Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...] Options are: -l list available Phabricator installations -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Invoke a command-line tool within the home directory of the named Phabricator installation. """, "l" -> (_ => list = true), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.isEmpty && !list) getopts.usage() val progress = new Console_Progress if (list) { for (config <- read_config()) { progress.echo("phabricator " + quote(config.name) + " root " + config.root) } } val config = get_config(name) val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true) if (!result.ok) error("Return code: " + result.rc.toString) }) /** setup **/ def user_setup(name: String, description: String, ssh_setup: Boolean = false) { if (!Linux.user_exists(name)) { Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup) } else if (Linux.user_description(name) != description) { error("User " + quote(name) + " already exists --" + " for Phabricator it should have the description:\n " + quote(description)) } } def phabricator_setup( name: String = default_name, root: String = "", repo: String = "", package_update: Boolean = false, progress: Progress = No_Progress) { /* system environment */ Linux.check_system_root() progress.echo("System packages ...") if (package_update) { Linux.package_update(progress = progress) Linux.check_reboot_required() } Linux.package_install(packages, progress = progress) Linux.check_reboot_required() /* users */ if (name == daemon_user) { error("Clash of installation name with daemon user " + quote(daemon_user)) } user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true) user_setup(name, "Phabricator SSH User") /* basic installation */ progress.echo("\nPhabricator installation ...") val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name) val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name) val configs = read_config() for (config <- configs if config.name == name) { error("Duplicate Phabricator installation " + quote(name) + " in " + config.root) } if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) { error("Failed to create root directory " + root_path) } progress.bash(cwd = root_path.file, echo = true, script = """ set -e chown """ + Bash.string(www_user) + ":" + Bash.string(www_user) + """ . chmod 755 . git clone https://github.com/phacility/libphutil.git git clone https://github.com/phacility/arcanist.git git clone https://github.com/phacility/phabricator.git """).check val config = Config(name, root_path) write_config(configs ::: List(config)) config.execute("config set pygments.enabled true") /* local repository directory */ progress.echo("\nRepository hosting setup ...") if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) { error("Failed to create local repository directory " + repo_path) } - Isabelle_System.bash(cwd = repo_path.file, - script = """ - set -e - chown -R """ + Bash.string(daemon_user) + ":" + Bash.string(daemon_user) + """ . - chmod 755 . - """).check + Isabelle_System.chown( + "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path) + Isabelle_System.chmod("755", repo_path) config.execute("config set repository.default-local-path " + File.bash_path(repo_path)) val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name()) File.write(sudoers_file, www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" + name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n") - Isabelle_System.bash("chmod 0440 " + File.bash_path(sudoers_file)).check + Isabelle_System.chmod("0440", sudoers_file) config.execute("config set diffusion.ssh-user " + Bash.string(config.name)) /* MySQL setup */ progress.echo("\nMySQL setup ...") File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")), """[mysqld] max_allowed_packet = 32M innodb_buffer_pool_size = 1600M local_infile = 0 """) Linux.service_restart("mysql") def mysql_conf(R: Regex): Option[String] = split_lines(File.read(Path.explode("/etc/mysql/debian.cnf"))).collectFirst({ case R(a) => a }) for (user <- mysql_conf("""^user\s*=\s*(\S*)\s*$""".r)) { config.execute("config set mysql.user " + Bash.string(user)) } for (pass <- mysql_conf("""^password\s*=\s*(\S*)\s*$""".r)) { config.execute("config set mysql.pass " + Bash.string(pass)) } config.execute("config set storage.default-namespace " + Bash.string(phabricator_name(name = name).replace("-", "_"))) config.execute("config set storage.mysql-engine.max-size 8388608") progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check /* PHP setup */ val php_version = Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""") .check.out val php_conf = Path.explode("/etc/php") + Path.basic(php_version) + // educated guess Path.explode("apache2/conf.d") + Path.basic(isabelle_phabricator_name(ext = "ini")) File.write(php_conf, "post_max_size = 32M\n" + "opcache.validate_timestamps = 0\n" + "memory_limit = 512M\n") /* Apache setup */ progress.echo("Apache setup ...") val apache_root = Path.explode("/etc/apache2") val apache_sites = apache_root + Path.explode("sites-available") if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites) val server_name = phabricator_name(name = name, ext = "lvh.me") // alias for "localhost" for testing val server_url = "http://" + server_name File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")), """ ServerName """ + server_name + """ ServerAdmin webmaster@localhost DocumentRoot """ + config.home.implode + """/webroot ErrorLog ${APACHE_LOG_DIR}/error.log RewriteEngine on RewriteRule ^(.*)$ /index.php?__path__=$1 [B,L,QSA] # vim: syntax=apache ts=4 sw=4 sts=4 sr noet """) Isabelle_System.bash( """ set -e a2enmod rewrite a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check config.execute("config set phabricator.base-uri " + Bash.string(server_url)) Linux.service_restart("apache2") /* PHP daemon */ progress.echo("PHP daemon setup ...") config.execute("config set phd.user " + Bash.string(daemon_user)) config.execute("config set phd.log-directory /var/tmp/phd/" + isabelle_phabricator_name(name = name) + "/log") Linux.service_install(isabelle_phabricator_name(name = name), """[Unit] Description=PHP daemon for Isabelle/Phabricator """ + quote(name) + """ After=syslog.target network.target apache2.service mysql.service [Service] Type=oneshot User=""" + daemon_user + """ Group=""" + daemon_user + """ Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin ExecStart=""" + config.home.implode + """/bin/phd start --force ExecStop=""" + config.home.implode + """/bin/phd stop RemainAfterExit=yes [Install] WantedBy=multi-user.target """) progress.echo("\nDONE\nWeb configuration via " + server_url) } /* Isabelle tool wrapper */ val isabelle_tool2 = Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args => { var repo = "" var package_update = false var name = default_name var root = "" val getopts = Getopts(""" Usage: isabelle phabricator_setup [OPTIONS] Options are: -R DIR repository directory (default: """ + default_repo("NAME") + """) -U full update of system packages before installation -n NAME Phabricator installation name (default: """ + quote(default_name) + """) -r DIR installation root directory (default: """ + default_root("NAME") + """) Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). The installation name (default: """ + quote(default_name) + """) is mapped to a regular Unix user; this is relevant for public SSH access. """, "R:" -> (arg => repo = arg), "U" -> (_ => package_update = true), "n:" -> (arg => name = arg), "r:" -> (arg => root = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup(name = name, root = root, repo = repo, package_update = package_update, progress = progress) }) /** setup mail **/ val mailers_template: String = """[ { "key": "example.org", "type": "smtp", "options": { "host": "mail.example.org", "port": 465, "user": "phabricator@example.org", "password": "********", "protocol": "ssl", "message-id": true } } ]""" def phabricator_setup_mail( name: String = default_name, config_file: Option[Path] = None, test_user: String = "", progress: Progress = No_Progress) { Linux.check_system_root() val config = get_config(name) val default_config_file = config.root + default_mailers val mail_config = config_file getOrElse default_config_file def setup_mail { progress.echo("Using mail configuration from " + mail_config) config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config)) if (test_user.nonEmpty) { progress.echo("Sending test mail to " + quote(test_user)) progress.bash(cwd = config.home.file, echo = true, script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ + Bash.string(test_user)).check } } if (config_file.isEmpty) { if (!default_config_file.is_file) { File.write(default_config_file, mailers_template) - Isabelle_System.bash("chmod 600 " + File.bash_path(default_config_file)).check + Isabelle_System.chmod("600", default_config_file) } if (File.read(default_config_file) == mailers_template) { progress.echo( """ Please invoke the tool again, after providing details in """ + default_config_file.implode + """ See also section "Mailer: SMTP" in https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email """) } else setup_mail } else setup_mail } /* Isabelle tool wrapper */ val isabelle_tool3 = Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phabricator installation", args => { var test_user = "" var name = default_name var config_file: Option[Path] = None val getopts = Getopts(""" Usage: isabelle phabricator_setup_mail [OPTIONS] Options are: -T USER send test mail to Phabricator user -f FILE config file (default: """ + default_mailers + """ within Phabricator root) -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Provide mail configuration for existing Phabricator installation. """, "T:" -> (arg => test_user = arg), "f:" -> (arg => config_file = Some(Path.explode(arg))), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_mail(name = name, config_file = config_file, test_user = test_user, progress = progress) }) /** setup ssh **/ /* sshd config */ private val Port = """^\s*Port\s+(\d+)\s*$""".r private val No_Port = """^#\s*Port\b.*$""".r private val Any_Port = """^#?\s*Port\b.*$""".r def conf_ssh_port(port: Int): String = if (port == 22) "#Port 22" else "Port " + port def read_ssh_port(conf: Path): Int = { val lines = split_lines(File.read(conf)) val ports = lines.flatMap({ case Port(Value.Int(p)) => Some(p) case No_Port() => Some(22) case _ => None }) ports match { case List(port) => port case Nil => error("Missing Port specification in " + conf) case _ => error("Multiple Port specifications in " + conf) } } def write_ssh_port(conf: Path, port: Int): Boolean = { val old_port = read_ssh_port(conf) if (old_port == port) false else { val lines = split_lines(File.read(conf)) val lines1 = lines.map({ case Any_Port() => conf_ssh_port(port) case line => line }) File.write(conf, cat_lines(lines1)) true } } /* phabricator_setup_ssh */ def phabricator_setup_ssh( server_port: Int = default_server_port, system_port: Int = default_system_port, test_server: Boolean = false, progress: Progress = No_Progress) { Linux.check_system_root() val configs = read_config() if (server_port == system_port) { error("Port for Phabricator sshd coincides with system port: " + system_port) } val sshd_conf_system = Path.explode("/etc/ssh/sshd_config") val sshd_conf_server = sshd_conf_system.ext(isabelle_phabricator_name()) val ssh_name = isabelle_phabricator_name(name = "ssh") val ssh_command = Path.explode("/usr/local/bin") + Path.basic(ssh_name) Linux.service_shutdown(ssh_name) val old_system_port = read_ssh_port(sshd_conf_system) if (old_system_port != system_port) { progress.echo("Reconfigurig system ssh service") Linux.service_shutdown("ssh") write_ssh_port(sshd_conf_system, system_port) Linux.service_start("ssh") } progress.echo("Configuring " + ssh_name + " service") File.write(ssh_command, """#!/bin/bash { while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } do NAME="$(echo "$REPLY" | cut -d: -f1)" ROOT="$(echo "$REPLY" | cut -d: -f2)" if [ "$1" = "$NAME" ] then exec "$ROOT/phabricator/bin/ssh-auth" "$@" fi done exit 1 } < /etc/isabelle-phabricator.conf """) - Isabelle_System.bash("chmod 755 " + File.bash_path(ssh_command)).check - Isabelle_System.bash("chown root:root " + File.bash_path(ssh_command)).check + Isabelle_System.chmod("755", ssh_command) + Isabelle_System.chown("root:root", ssh_command) File.write(sshd_conf_server, """# OpenBSD Secure Shell server for Isabelle/Phabricator AuthorizedKeysCommand """ + ssh_command.implode + """ AuthorizedKeysCommandUser """ + daemon_user + """ AuthorizedKeysFile none AllowUsers """ + configs.map(_.name).mkString(" ") + """ Port """ + server_port + """ Protocol 2 PermitRootLogin no AllowAgentForwarding no AllowTcpForwarding no PrintMotd no PrintLastLog no PasswordAuthentication no ChallengeResponseAuthentication no PidFile /var/run/""" + ssh_name + """.pid """) Linux.service_install(ssh_name, """[Unit] Description=OpenBSD Secure Shell server for Isabelle/Phabricator After=network.target auditd.service ConditionPathExists=!/etc/ssh/sshd_not_to_be_run [Service] EnvironmentFile=-/etc/default/ssh ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecStart=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -D $SSHD_OPTS ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecReload=/bin/kill -HUP $MAINPID KillMode=process Restart=on-failure RestartPreventExitStatus=255 Type=notify RuntimeDirectory=sshd-phabricator RuntimeDirectoryMode=0755 [Install] WantedBy=multi-user.target Alias=""" + ssh_name + """.service """) for (config <- configs) { progress.echo("phabricator " + quote(config.name) + " port " + server_port) config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString)) if (test_server) { progress.bash( """unset DISPLAY echo "{}" | ssh -p """ + Bash.string(server_port.toString) + " -o StrictHostKeyChecking=false " + Bash.string(config.name) + """@localhost conduit conduit.ping""").print } } } /* Isabelle tool wrapper */ val isabelle_tool4 = Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phabricator installations", args => { var server_port = default_server_port var system_port = default_system_port var test_server = false val getopts = Getopts(""" Usage: isabelle phabricator_setup_ssh [OPTIONS] Options are: -p PORT sshd port for Phabricator servers (default: """ + default_server_port + """) -q PORT sshd port for the operating system (default: """ + default_system_port + """) -T test the ssh service for each Phabricator installation Configure ssh service for all Phabricator installations: a separate sshd is run in addition to the one of the operating system, and ports need to be distinct. A particular Phabricator installation is addressed by using its name as the ssh user; the actual Phabricator user is determined via stored ssh keys. """, "p:" -> (arg => server_port = Value.Int.parse(arg)), "q:" -> (arg => system_port = Value.Int.parse(arg)), "T" -> (_ => test_server = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_ssh( server_port = server_port, system_port = system_port, test_server = test_server, progress = progress) }) } diff --git a/src/Pure/Tools/server.scala b/src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala +++ b/src/Pure/Tools/server.scala @@ -1,619 +1,619 @@ /* Title: Pure/Tools/server.scala Author: Makarius Resident Isabelle servers. Message formats: - short message (single line): NAME ARGUMENT - long message (multiple lines): BYTE_LENGTH NAME ARGUMENT Argument formats: - Unit as empty string - XML.Elem in YXML notation - JSON.T in standard notation */ package isabelle import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter, IOException} import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress} object Server { /* message argument */ object Argument { def is_name_char(c: Char): Boolean = Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || c == '_' || c == '.' def split(msg: String): (String, String) = { val name = msg.takeWhile(is_name_char(_)) val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_)) (name, argument) } def print(arg: Any): String = arg match { case () => "" case t: XML.Elem => YXML.string_of_tree(t) case t: JSON.T => JSON.Format(t) } def parse(argument: String): Any = if (argument == "") () else if (YXML.detect_elem(argument)) YXML.parse_elem(argument) else JSON.parse(argument, strict = false) def unapply(argument: String): Option[Any] = try { Some(parse(argument)) } catch { case ERROR(_) => None } } /* input command */ object Command { type T = PartialFunction[(Context, Any), Any] private val table: Map[String, T] = Map( "help" -> { case (_, ()) => table.keySet.toList.sorted }, "echo" -> { case (_, t) => t }, "shutdown" -> { case (context, ()) => context.server.shutdown() }, "cancel" -> { case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) }, "session_build" -> { case (context, Server_Commands.Session_Build(args)) => context.make_task(task => Server_Commands.Session_Build.command(args, progress = task.progress)._1) }, "session_start" -> { case (context, Server_Commands.Session_Start(args)) => context.make_task(task => { val (res, entry) = Server_Commands.Session_Start.command( args, progress = task.progress, log = context.server.log) context.server.add_session(entry) res }) }, "session_stop" -> { case (context, Server_Commands.Session_Stop(id)) => context.make_task(_ => { val session = context.server.remove_session(id) Server_Commands.Session_Stop.command(session)._1 }) }, "use_theories" -> { case (context, Server_Commands.Use_Theories(args)) => context.make_task(task => { val session = context.server.the_session(args.session_id) Server_Commands.Use_Theories.command( args, session, id = task.id, progress = task.progress)._1 }) }, "purge_theories" -> { case (context, Server_Commands.Purge_Theories(args)) => val session = context.server.the_session(args.session_id) Server_Commands.Purge_Theories.command(args, session)._1 }) def unapply(name: String): Option[T] = table.get(name) } /* output reply */ class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty) extends RuntimeException(message) def json_error(exn: Throwable): JSON.Object.T = exn match { case e: Error => Reply.error_message(e.message) ++ e.json case ERROR(msg) => Reply.error_message(msg) case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn)) case _ => JSON.Object.empty } object Reply extends Enumeration { val OK, ERROR, FINISHED, FAILED, NOTE = Value def message(msg: String, kind: String = ""): JSON.Object.T = JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg) def error_message(msg: String): JSON.Object.T = message(msg, kind = Markup.ERROR) def unapply(msg: String): Option[(Reply.Value, Any)] = { if (msg == "") None else { val (name, argument) = Argument.split(msg) for { reply <- try { Some(withName(name)) } catch { case _: NoSuchElementException => None } arg <- Argument.unapply(argument) } yield (reply, arg) } } } /* socket connection */ object Connection { def apply(socket: Socket): Connection = new Connection(socket) } class Connection private(socket: Socket) extends AutoCloseable { override def toString: String = socket.toString def close() { socket.close } def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) } private val in = new BufferedInputStream(socket.getInputStream) private val out = new BufferedOutputStream(socket.getOutputStream) private val out_lock: AnyRef = new Object def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop = new TTY_Loop( new OutputStreamWriter(out), new InputStreamReader(in), writer_lock = out_lock, interrupt = interrupt) def read_password(password: String): Boolean = try { Byte_Message.read_line(in).map(_.text) == Some(password) } catch { case _: IOException => false } def read_message(): Option[String] = try { Byte_Message.read_line_message(in).map(_.text) } catch { case _: IOException => None } def write_message(msg: String): Unit = out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) } def reply(r: Reply.Value, arg: Any) { val argument = Argument.print(arg) write_message(if (argument == "") r.toString else r.toString + " " + argument) } def reply_ok(arg: Any) { reply(Reply.OK, arg) } def reply_error(arg: Any) { reply(Reply.ERROR, arg) } def reply_error_message(message: String, more: JSON.Object.Entry*): Unit = reply_error(Reply.error_message(message) ++ more) def notify(arg: Any) { reply(Reply.NOTE, arg) } } /* context with output channels */ class Context private[Server](val server: Server, connection: Connection) extends AutoCloseable { context => def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) } def notify(arg: Any) { connection.notify(arg) } def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit = notify(Reply.message(msg, kind = kind) ++ more) def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*) def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*) def error_message(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.ERROR, msg, more:_*) def progress(more: JSON.Object.Entry*): Connection_Progress = new Connection_Progress(context, more:_*) override def toString: String = connection.toString /* asynchronous tasks */ private val _tasks = Synchronized(Set.empty[Task]) def make_task(body: Task => JSON.Object.T): Task = { val task = new Task(context, body) _tasks.change(_ + task) task } def remove_task(task: Task): Unit = _tasks.change(_ - task) def cancel_task(id: UUID.T): Unit = _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks }) def close() { while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) })) { _tasks.value.foreach(_.join) } } } class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*) extends Progress { override def echo(msg: String): Unit = context.writeln(msg, more:_*) override def echo_warning(msg: String): Unit = context.warning(msg, more:_*) override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*) override def theory(theory: Progress.Theory) { val entries: List[JSON.Object.Entry] = List("theory" -> theory.theory, "session" -> theory.session) ::: (theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) }) context.writeln(theory.message, entries ::: more.toList:_*) } override def nodes_status(nodes_status: Document_Status.Nodes_Status) { val json = for ((name, node_status) <- nodes_status.present) yield name.json + ("status" -> nodes_status(name).json) context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json)) } @volatile private var is_stopped = false override def stopped: Boolean = is_stopped def stop { is_stopped = true } override def toString: String = context.toString } class Task private[Server](val context: Context, body: Task => JSON.Object.T) { task => val id: UUID.T = UUID.random() val ident: JSON.Object.Entry = ("task" -> id.toString) val progress: Connection_Progress = context.progress(ident) def cancel { progress.stop } private lazy val thread = Standard_Thread.fork("server_task") { Exn.capture { body(task) } match { case Exn.Res(res) => context.reply(Reply.FINISHED, res + ident) case Exn.Exn(exn) => val err = json_error(exn) if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident) } progress.stop context.remove_task(task) } def start { thread } def join { thread.join } } /* server info */ val localhost_name: String = "127.0.0.1" def localhost: InetAddress = InetAddress.getByName(localhost_name) def print_address(port: Int): String = localhost_name + ":" + port def print(port: Int, password: String): String = print_address(port) + " (password " + quote(password) + ")" object Info { private val Pattern = ("""server "([^"]*)" = \Q""" + localhost_name + """\E:(\d+) \(password "([^"]*)"\)""").r def parse(s: String): Option[Info] = s match { case Pattern(name, Value.Int(port), password) => Some(Info(name, port, password)) case _ => None } def apply(name: String, port: Int, password: String): Info = new Info(name, port, password) } class Info private(val name: String, val port: Int, val password: String) { def address: String = print_address(port) override def toString: String = "server " + quote(name) + " = " + print(port, password) def connection(): Connection = { val connection = Connection(new Socket(localhost, port)) connection.write_message(password) connection } def active(): Boolean = try { using(connection())(connection => { connection.set_timeout(Time.seconds(2.0)) connection.read_message() match { case Some(Reply(Reply.OK, _)) => true case _ => false } }) } catch { case _: IOException => false case _: SocketException => false case _: SocketTimeoutException => false } } /* per-user servers */ val default_name = "isabelle" object Data { val database = Path.explode("$ISABELLE_HOME_USER/servers.db") val name = SQL.Column.string("name").make_primary_key val port = SQL.Column.int("port") val password = SQL.Column.string("password") val table = SQL.Table("isabelle_servers", List(name, port, password)) } def list(db: SQLite.Database): List[Info] = if (db.tables.contains(Data.table.name)) { db.using_statement(Data.table.select())(stmt => stmt.execute_query().iterator(res => Info( res.string(Data.name), res.int(Data.port), res.string(Data.password))).toList.sortBy(_.name)) } else Nil def find(db: SQLite.Database, name: String): Option[Info] = list(db).find(server_info => server_info.name == name && server_info.active) def init( name: String = default_name, port: Int = 0, existing_server: Boolean = false, log: Logger = No_Logger): (Info, Option[Server]) = { using(SQLite.open_database(Data.database))(db => { db.transaction { - Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check + Isabelle_System.chmod("600", Data.database) db.create_table(Data.table) list(db).filterNot(_.active).foreach(server_info => db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))( _.execute)) } db.transaction { find(db, name) match { case Some(server_info) => (server_info, None) case None => if (existing_server) error("Isabelle server " + quote(name) + " not running") val server = new Server(port, log) val server_info = Info(name, server.port, server.password) db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute) db.using_statement(Data.table.insert())(stmt => { stmt.string(1) = server_info.name stmt.int(2) = server_info.port stmt.string(3) = server_info.password stmt.execute() }) server.start (server_info, Some(server)) } } }) } def exit(name: String = default_name): Boolean = { using(SQLite.open_database(Data.database))(db => db.transaction { find(db, name) match { case Some(server_info) => using(server_info.connection())(_.write_message("shutdown")) while(server_info.active) { Thread.sleep(50) } true case None => false } }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("server", "manage resident Isabelle servers", args => { var console = false var log_file: Option[Path] = None var operation_list = false var operation_exit = false var name = default_name var port = 0 var existing_server = false val getopts = Getopts(""" Usage: isabelle server [OPTIONS] Options are: -L FILE logging on FILE -c console interaction with specified server -l list servers (alternative operation) -n NAME explicit server name (default: """ + default_name + """) -p PORT explicit server port -s assume existing server, no implicit startup -x exit specified server (alternative operation) Manage resident Isabelle servers. """, "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))), "c" -> (_ => console = true), "l" -> (_ => operation_list = true), "n:" -> (arg => name = arg), "p:" -> (arg => port = Value.Int.parse(arg)), "s" -> (_ => existing_server = true), "x" -> (_ => operation_exit = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() if (operation_list) { for { server_info <- using(SQLite.open_database(Data.database))(list(_)) if server_info.active } Output.writeln(server_info.toString, stdout = true) } else if (operation_exit) { val ok = Server.exit(name) sys.exit(if (ok) 0 else 2) } else { val log = Logger.make(log_file) val (server_info, server) = init(name, port = port, existing_server = existing_server, log = log) Output.writeln(server_info.toString, stdout = true) if (console) { using(server_info.connection())(connection => connection.tty_loop().join) } server.foreach(_.join) } }) } class Server private(_port: Int, val log: Logger) { server => private val server_socket = new ServerSocket(_port, 50, Server.localhost) private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session]) def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString)) def the_session(id: UUID.T): Headless.Session = _sessions.value.get(id) getOrElse err_session(id) def add_session(entry: (UUID.T, Headless.Session)) { _sessions.change(_ + entry) } def remove_session(id: UUID.T): Headless.Session = { _sessions.change_result(sessions => sessions.get(id) match { case Some(session) => (session, sessions - id) case None => err_session(id) }) } def shutdown() { server_socket.close val sessions = _sessions.change_result(sessions => (sessions, Map.empty)) for ((_, session) <- sessions) { try { val result = session.stop() if (!result.ok) log("Session shutdown failed: return code " + result.rc) } catch { case ERROR(msg) => log("Session shutdown failed: " + msg) } } } def port: Int = server_socket.getLocalPort val password: String = UUID.random_string() override def toString: String = Server.print(port, password) private def handle(connection: Server.Connection) { using(new Server.Context(server, connection))(context => { if (connection.read_password(password)) { connection.reply_ok( JSON.Object( "isabelle_id" -> Isabelle_System.isabelle_id(), "isabelle_version" -> Distribution.version)) var finished = false while (!finished) { connection.read_message() match { case None => finished = true case Some("") => context.notify("Command 'help' provides list of commands") case Some(msg) => val (name, argument) = Server.Argument.split(msg) name match { case Server.Command(cmd) => argument match { case Server.Argument(arg) => if (cmd.isDefinedAt((context, arg))) { Exn.capture { cmd((context, arg)) } match { case Exn.Res(task: Server.Task) => connection.reply_ok(JSON.Object(task.ident)) task.start case Exn.Res(res) => connection.reply_ok(res) case Exn.Exn(exn) => val err = Server.json_error(exn) if (err.isEmpty) throw exn else connection.reply_error(err) } } else { connection.reply_error_message( "Bad argument for command " + Library.single_quote(name), "argument" -> argument) } case _ => connection.reply_error_message( "Malformed argument for command " + Library.single_quote(name), "argument" -> argument) } case _ => connection.reply_error("Bad command " + Library.single_quote(name)) } } } } }) } private lazy val server_thread: Thread = Standard_Thread.fork("server") { var finished = false while (!finished) { Exn.capture(server_socket.accept) match { case Exn.Res(socket) => Standard_Thread.fork("server_connection") { using(Server.Connection(socket))(handle(_)) } case Exn.Exn(_) => finished = true } } } def start { server_thread } def join { server_thread.join; shutdown() } }