--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Fri Apr 01 23:19:12 2022 +0200
@@ -109,32 +109,33 @@
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools",
- Scala_Project.here, args => {
- val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
+ Scala_Project.here,
+ { args =>
+ val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
- var options = Options.init(opts = build_options)
- val mirabelle_dry_run = options.check_name("mirabelle_dry_run")
- val mirabelle_max_calls = options.check_name("mirabelle_max_calls")
- val mirabelle_randomize = options.check_name("mirabelle_randomize")
- val mirabelle_stride = options.check_name("mirabelle_stride")
- val mirabelle_timeout = options.check_name("mirabelle_timeout")
- val mirabelle_output_dir = options.check_name("mirabelle_output_dir")
+ var options = Options.init(opts = build_options)
+ val mirabelle_dry_run = options.check_name("mirabelle_dry_run")
+ val mirabelle_max_calls = options.check_name("mirabelle_max_calls")
+ val mirabelle_randomize = options.check_name("mirabelle_randomize")
+ val mirabelle_stride = options.check_name("mirabelle_stride")
+ val mirabelle_timeout = options.check_name("mirabelle_timeout")
+ val mirabelle_output_dir = options.check_name("mirabelle_output_dir")
- var actions: List[String] = Nil
- var base_sessions: List[String] = Nil
- var select_dirs: List[Path] = Nil
- var numa_shuffling = false
- var output_dir = Path.explode(mirabelle_output_dir.default_value)
- var theories: List[String] = Nil
- var exclude_session_groups: List[String] = Nil
- var all_sessions = false
- var dirs: List[Path] = Nil
- var session_groups: List[String] = Nil
- var max_jobs = 1
- var verbose = false
- var exclude_sessions: List[String] = Nil
+ var actions: List[String] = Nil
+ var base_sessions: List[String] = Nil
+ var select_dirs: List[Path] = Nil
+ var numa_shuffling = false
+ var output_dir = Path.explode(mirabelle_output_dir.default_value)
+ var theories: List[String] = Nil
+ var exclude_session_groups: List[String] = Nil
+ var all_sessions = false
+ var dirs: List[Path] = Nil
+ var session_groups: List[String] = Nil
+ var max_jobs = 1
+ var verbose = false
+ var exclude_sessions: List[String] = Nil
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...]
Options are:
@@ -170,69 +171,69 @@
Available actions are:""" + action_names().mkString("\n ", "\n ", "") + """
For the ACTION "sledgehammer", the usual sledgehammer as well as the following mirabelle-specific OPTIONs are available:""" +
- sledgehammer_options().mkString("\n ", "\n ", "\n"),
- "A:" -> (arg => actions = actions ::: List(arg)),
- "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
- "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
- "N" -> (_ => numa_shuffling = true),
- "O:" -> (arg => output_dir = Path.explode(arg)),
- "T:" -> (arg => theories = theories ::: List(arg)),
- "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
- "a" -> (_ => all_sessions = true),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "g:" -> (arg => session_groups = session_groups ::: List(arg)),
- "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
- "m:" -> (arg => options = options + ("mirabelle_max_calls=" + arg)),
- "o:" -> (arg => options = options + arg),
- "r:" -> (arg => options = options + ("mirabelle_randomize=" + arg)),
- "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)),
- "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)),
- "v" -> (_ => verbose = true),
- "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)),
- "y" -> (arg => options = options + ("mirabelle_dry_run=true")))
-
- val sessions = getopts(args)
- if (actions.isEmpty) getopts.usage()
+ sledgehammer_options().mkString("\n ", "\n ", "\n"),
+ "A:" -> (arg => actions = actions ::: List(arg)),
+ "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
+ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "N" -> (_ => numa_shuffling = true),
+ "O:" -> (arg => output_dir = Path.explode(arg)),
+ "T:" -> (arg => theories = theories ::: List(arg)),
+ "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+ "a" -> (_ => all_sessions = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+ "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+ "m:" -> (arg => options = options + ("mirabelle_max_calls=" + arg)),
+ "o:" -> (arg => options = options + arg),
+ "r:" -> (arg => options = options + ("mirabelle_randomize=" + arg)),
+ "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)),
+ "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)),
+ "v" -> (_ => verbose = true),
+ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)),
+ "y" -> (arg => options = options + ("mirabelle_dry_run=true")))
- val progress = new Console_Progress(verbose = verbose)
-
- val start_date = Date.now()
+ val sessions = getopts(args)
+ if (actions.isEmpty) getopts.usage()
- if (verbose) {
- progress.echo("Started at " + Build_Log.print_date(start_date))
- }
+ val progress = new Console_Progress(verbose = verbose)
- val results =
- progress.interrupt_handler {
- mirabelle(options, actions, output_dir.absolute,
- theories = theories,
- selection = Sessions.Selection(
- all_sessions = all_sessions,
- base_sessions = base_sessions,
- exclude_session_groups = exclude_session_groups,
- exclude_sessions = exclude_sessions,
- session_groups = session_groups,
- sessions = sessions),
- progress = progress,
- dirs = dirs,
- select_dirs = select_dirs,
- numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
- max_jobs = max_jobs,
- verbose = verbose)
+ val start_date = Date.now()
+
+ if (verbose) {
+ progress.echo("Started at " + Build_Log.print_date(start_date))
}
- val end_date = Date.now()
- val elapsed_time = end_date.time - start_date.time
-
- if (verbose) {
- progress.echo("\nFinished at " + Build_Log.print_date(end_date))
- }
+ val results =
+ progress.interrupt_handler {
+ mirabelle(options, actions, output_dir.absolute,
+ theories = theories,
+ selection = Sessions.Selection(
+ all_sessions = all_sessions,
+ base_sessions = base_sessions,
+ exclude_session_groups = exclude_session_groups,
+ exclude_sessions = exclude_sessions,
+ session_groups = session_groups,
+ sessions = sessions),
+ progress = progress,
+ dirs = dirs,
+ select_dirs = select_dirs,
+ numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
+ max_jobs = max_jobs,
+ verbose = verbose)
+ }
- val total_timing =
- results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
- copy(elapsed = elapsed_time)
- progress.echo(total_timing.message_resources)
+ val end_date = Date.now()
+ val elapsed_time = end_date.time - start_date.time
+
+ if (verbose) {
+ progress.echo("\nFinished at " + Build_Log.print_date(end_date))
+ }
- sys.exit(results.rc)
- })
+ val total_timing =
+ results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
+ copy(elapsed = elapsed_time)
+ progress.echo(total_timing.message_resources)
+
+ sys.exit(results.rc)
+ })
}
--- a/src/Pure/Admin/build_csdp.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_csdp.scala Fri Apr 01 23:19:12 2022 +0200
@@ -56,7 +56,7 @@
): Unit = {
mingw.check
- Isabelle_System.with_tmp_dir("build")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
@@ -159,7 +159,7 @@
Makarius
""" + Date.Format.date(Date.now()) + "\n")
- })
+ }
}
@@ -167,13 +167,13 @@
val isabelle_tool =
Isabelle_Tool("build_csdp", "build prover component from official download", Scala_Project.here,
- args => {
- var target_dir = Path.current
- var mingw = MinGW.none
- var download_url = default_download_url
- var verbose = false
+ { args =>
+ var target_dir = Path.current
+ var mingw = MinGW.none
+ var download_url = default_download_url
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_csdp [OPTIONS]
Options are:
@@ -185,17 +185,17 @@
Build prover component from official download.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "M:" -> (arg => mingw = MinGW(Path.explode(arg))),
- "U:" -> (arg => download_url = arg),
- "v" -> (_ => verbose = true))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "M:" -> (arg => mingw = MinGW(Path.explode(arg))),
+ "U:" -> (arg => download_url = arg),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_csdp(download_url = download_url, verbose = verbose, progress = progress,
- target_dir = target_dir, mingw = mingw)
- })
+ build_csdp(download_url = download_url, verbose = verbose, progress = progress,
+ target_dir = target_dir, mingw = mingw)
+ })
}
--- a/src/Pure/Admin/build_cygwin.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_cygwin.scala Fri Apr 01 23:19:12 2022 +0200
@@ -19,7 +19,7 @@
): Unit = {
require(Platform.is_windows, "Windows platform expected")
- Isabelle_System.with_tmp_dir("cygwin")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("cygwin") { tmp_dir =>
val cygwin = tmp_dir + Path.explode("cygwin")
val cygwin_etc = cygwin + Path.explode("etc")
val cygwin_isabelle = Isabelle_System.make_directory(cygwin + Path.explode("isabelle"))
@@ -52,7 +52,7 @@
val archive = "cygwin-" + Date.Format.alt_date(Date.now()) + ".tar.gz"
Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check
- })
+ }
}
@@ -60,12 +60,13 @@
val isabelle_tool =
Isabelle_Tool("build_cygwin", "produce pre-canned Cygwin distribution for Isabelle",
- Scala_Project.here, args => {
- var mirror = default_mirror
- var more_packages: List[String] = Nil
+ Scala_Project.here,
+ { args =>
+ var mirror = default_mirror
+ var more_packages: List[String] = Nil
- val getopts =
- Getopts("""
+ val getopts =
+ Getopts("""
Usage: isabelle build_cygwin [OPTIONS]
Options are:
@@ -75,12 +76,12 @@
Produce pre-canned Cygwin distribution for Isabelle: this requires
Windows administrator mode.
""",
- "R:" -> (arg => mirror = arg),
- "p:" -> (arg => more_packages ::= arg))
+ "R:" -> (arg => mirror = arg),
+ "p:" -> (arg => more_packages ::= arg))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- build_cygwin(new Console_Progress(), mirror = mirror, more_packages = more_packages)
- })
+ build_cygwin(new Console_Progress(), mirror = mirror, more_packages = more_packages)
+ })
}
--- a/src/Pure/Admin/build_doc.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_doc.scala Fri Apr 01 23:19:12 2022 +0200
@@ -73,14 +73,15 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here, args => {
- var all_docs = false
- var max_jobs = 1
- var sequential = false
- var options = Options.init()
+ Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here,
+ { args =>
+ var all_docs = false
+ var max_jobs = 1
+ var sequential = false
+ var options = Options.init()
- val getopts =
- Getopts("""
+ val getopts =
+ Getopts("""
Usage: isabelle build_doc [OPTIONS] [DOCS ...]
Options are:
@@ -92,20 +93,20 @@
Build Isabelle documentation from documentation sessions with
suitable document_variants entry.
""",
- "a" -> (_ => all_docs = true),
- "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
- "o:" -> (arg => options = options + arg),
- "s" -> (_ => sequential = true))
+ "a" -> (_ => all_docs = true),
+ "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+ "o:" -> (arg => options = options + arg),
+ "s" -> (_ => sequential = true))
- val docs = getopts(args)
+ val docs = getopts(args)
- if (!all_docs && docs.isEmpty) getopts.usage()
+ if (!all_docs && docs.isEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- progress.interrupt_handler {
- build_doc(options, progress = progress, all_docs = all_docs, max_jobs = max_jobs,
- sequential = sequential, docs = docs)
- }
- })
+ progress.interrupt_handler {
+ build_doc(options, progress = progress, all_docs = all_docs, max_jobs = max_jobs,
+ sequential = sequential, docs = docs)
+ }
+ })
}
--- a/src/Pure/Admin/build_e.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_e.scala Fri Apr 01 23:19:12 2022 +0200
@@ -20,7 +20,7 @@
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
- Isabelle_System.with_tmp_dir("build")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val component_name = "e-" + version
@@ -100,20 +100,20 @@
Makarius
""" + Date.Format.date(Date.now()) + "\n")
- })
+ }
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_e", "build prover component from source distribution", Scala_Project.here,
- args => {
- var target_dir = Path.current
- var version = default_version
- var download_url = default_download_url
- var verbose = false
+ { args =>
+ var target_dir = Path.current
+ var version = default_version
+ var download_url = default_download_url
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_e [OPTIONS]
Options are:
@@ -125,17 +125,17 @@
Build prover component from the specified source distribution.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "U:" -> (arg => download_url = arg),
- "V:" -> (arg => version = arg),
- "v" -> (_ => verbose = true))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => download_url = arg),
+ "V:" -> (arg => version = arg),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_e(version = version, download_url = download_url,
- verbose = verbose, progress = progress, target_dir = target_dir)
- })
+ build_e(version = version, download_url = download_url,
+ verbose = verbose, progress = progress, target_dir = target_dir)
+ })
}
--- a/src/Pure/Admin/build_fonts.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_fonts.scala Fri Apr 01 23:19:12 2022 +0200
@@ -238,7 +238,7 @@
val target_names = source_names.update(prefix = target_prefix, version = target_version)
- Isabelle_System.with_tmp_file("font", "ttf")(tmp_file => {
+ Isabelle_System.with_tmp_file("font", "ttf") { tmp_file =>
for (hinted <- hinting) {
val target_file = target_dir + hinted_path(hinted) + target_names.ttf
progress.echo("Font " + target_file.toString + " ...")
@@ -265,7 +265,7 @@
Fontforge.close)
).check
}
- })
+ }
(target_names.ttf, index)
}
@@ -336,10 +336,11 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_fonts", "construct Isabelle fonts", Scala_Project.here, args => {
- var source_dirs: List[Path] = Nil
+ Isabelle_Tool("build_fonts", "construct Isabelle fonts", Scala_Project.here,
+ { args =>
+ var source_dirs: List[Path] = Nil
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_fonts [OPTIONS]
Options are:
@@ -347,17 +348,17 @@
Construct Isabelle fonts from DejaVu font families and Isabelle symbols.
""",
- "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
+ "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val target_version = Date.Format.alt_date(Date.now())
- val target_dir = Path.explode("isabelle_fonts-" + target_version)
+ val target_version = Date.Format.alt_date(Date.now())
+ val target_dir = Path.explode("isabelle_fonts-" + target_version)
- val progress = new Console_Progress
+ val progress = new Console_Progress
- build_fonts(source_dirs = source_dirs, target_dir = target_dir,
- target_version = target_version, progress = progress)
- })
+ build_fonts(source_dirs = source_dirs, target_dir = target_dir,
+ target_version = target_version, progress = progress)
+ })
}
--- a/src/Pure/Admin/build_history.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_history.scala Fri Apr 01 23:19:12 2022 +0200
@@ -281,81 +281,81 @@
build_out_progress.echo("Reading session build info ...")
val session_build_info =
- build_info.finished_sessions.flatMap(session_name => {
- val database = isabelle_output + store.database(session_name)
+ build_info.finished_sessions.flatMap { session_name =>
+ val database = isabelle_output + store.database(session_name)
- if (database.is_file) {
- using(SQLite.open_database(database))(db => {
- val theory_timings =
- try {
- store.read_theory_timings(db, session_name).map(ps =>
- Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
- }
- catch { case ERROR(_) => Nil }
+ if (database.is_file) {
+ using(SQLite.open_database(database)) { db =>
+ val theory_timings =
+ try {
+ store.read_theory_timings(db, session_name).map(ps =>
+ Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
+ }
+ catch { case ERROR(_) => Nil }
- val session_sources =
- store.read_build(db, session_name).map(_.sources) match {
- case Some(sources) if sources.length == SHA1.digest_length =>
- List("Sources " + session_name + " " + sources)
- case _ => Nil
- }
+ val session_sources =
+ store.read_build(db, session_name).map(_.sources) match {
+ case Some(sources) if sources.length == SHA1.digest_length =>
+ List("Sources " + session_name + " " + sources)
+ case _ => Nil
+ }
- theory_timings ::: session_sources
- })
+ theory_timings ::: session_sources
}
- else Nil
- })
+ }
+ else Nil
+ }
build_out_progress.echo("Reading ML statistics ...")
val ml_statistics =
- build_info.finished_sessions.flatMap(session_name => {
- val database = isabelle_output + store.database(session_name)
- val log_gz = isabelle_output + store.log_gz(session_name)
+ build_info.finished_sessions.flatMap { session_name =>
+ val database = isabelle_output + store.database(session_name)
+ val log_gz = isabelle_output + store.log_gz(session_name)
- val properties =
- if (database.is_file) {
- using(SQLite.open_database(database))(db =>
- store.read_ml_statistics(db, session_name))
- }
- else if (log_gz.is_file) {
- Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
- }
- else Nil
+ val properties =
+ if (database.is_file) {
+ using(SQLite.open_database(database))(db =>
+ store.read_ml_statistics(db, session_name))
+ }
+ else if (log_gz.is_file) {
+ Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
+ }
+ else Nil
- val trimmed_properties =
- if (ml_statistics_step <= 0) Nil
- else if (ml_statistics_step == 1) properties
- else {
- (for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 }
- yield ps).toList
- }
+ val trimmed_properties =
+ if (ml_statistics_step <= 0) Nil
+ else if (ml_statistics_step == 1) properties
+ else {
+ (for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 }
+ yield ps).toList
+ }
- trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
- })
+ trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
+ }
build_out_progress.echo("Reading error messages ...")
val session_errors =
- build_info.failed_sessions.flatMap(session_name => {
- val database = isabelle_output + store.database(session_name)
- val errors =
- if (database.is_file) {
- try {
- using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
- } // column "errors" could be missing
- catch { case _: java.sql.SQLException => Nil }
- }
- else Nil
- errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg))
- })
+ build_info.failed_sessions.flatMap { session_name =>
+ val database = isabelle_output + store.database(session_name)
+ val errors =
+ if (database.is_file) {
+ try {
+ using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
+ } // column "errors" could be missing
+ catch { case _: java.sql.SQLException => Nil }
+ }
+ else Nil
+ errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg))
+ }
build_out_progress.echo("Reading heap sizes ...")
val heap_sizes =
- build_info.finished_sessions.flatMap(session_name => {
- val heap = isabelle_output + Path.explode(session_name)
- if (heap.is_file)
- Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
- else None
- })
+ build_info.finished_sessions.flatMap { session_name =>
+ val heap = isabelle_output + Path.explode(session_name)
+ if (heap.is_file)
+ Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
+ else None
+ }
build_out_progress.echo("Writing log file " + log_path.xz + " ...")
File.write_xz(log_path.xz,
@@ -583,7 +583,7 @@
/* Admin/build_history */
- ssh.with_tmp_dir(tmp_dir => {
+ ssh.with_tmp_dir { tmp_dir =>
val output_file = tmp_dir + Path.explode("output")
val rev_options = if (rev == "") "" else " -r " + Bash.string(rev_id)
@@ -607,6 +607,6 @@
ssh.rm(log)
(log.file_name, bytes)
}
- })
+ }
}
}
--- a/src/Pure/Admin/build_jcef.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_jcef.scala Fri Apr 01 23:19:12 2022 +0200
@@ -60,7 +60,7 @@
val platform_settings: List[String] =
for (platform <- platforms) yield {
- Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_file => {
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_file =>
val url = base_url + "/" + version + "/" + platform.archive
Isabelle_System.download_file(url, archive_file, progress = progress)
@@ -85,7 +85,7 @@
" " + "ISABELLE_JCEF_LIB=\"$ISABELLE_JCEF_HOME/" + platform.lib + "\"\n" +
" " + platform.library + "\n" +
" " + ";;"
- })
+ }
}
@@ -142,12 +142,13 @@
val isabelle_tool =
Isabelle_Tool("build_jcef", "build component for Java Chromium Embedded Framework",
- Scala_Project.here, args => {
- var target_dir = Path.current
- var base_url = default_url
- var version = default_version
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var base_url = default_url
+ var version = default_version
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_jcef [OPTIONS]
Options are:
@@ -157,16 +158,16 @@
Build component for Java Chromium Embedded Framework.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "U:" -> (arg => base_url = arg),
- "V:" -> (arg => version = arg))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => base_url = arg),
+ "V:" -> (arg => version = arg))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_jcef(base_url = base_url, version = version, target_dir = target_dir,
- progress = progress)
- })
+ build_jcef(base_url = base_url, version = version, target_dir = target_dir,
+ progress = progress)
+ })
}
--- a/src/Pure/Admin/build_jdk.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_jdk.scala Fri Apr 01 23:19:12 2022 +0200
@@ -152,56 +152,56 @@
): Unit = {
if (Platform.is_windows) error("Cannot build jdk on Windows")
- Isabelle_System.with_tmp_dir("jdk")(dir => {
- progress.echo("Extracting ...")
- val platforms = archives.map(extract_archive(dir, _))
+ Isabelle_System.with_tmp_dir("jdk") { dir =>
+ progress.echo("Extracting ...")
+ val platforms = archives.map(extract_archive(dir, _))
- val jdk_version =
- platforms.map(_.jdk_version).distinct match {
- case List(version) => version
- case Nil => error("No archives")
- case versions =>
- error("Archives contain multiple JDK versions: " + commas_quote(versions))
- }
-
- templates.filterNot(p1 => platforms.exists(p2 => p1.platform_name == p2.platform_name))
- match {
- case Nil =>
- case missing => error("Missing platforms: " + commas_quote(missing.map(_.platform_name)))
+ val jdk_version =
+ platforms.map(_.jdk_version).distinct match {
+ case List(version) => version
+ case Nil => error("No archives")
+ case versions =>
+ error("Archives contain multiple JDK versions: " + commas_quote(versions))
}
- val jdk_name = "jdk-" + jdk_version
- val jdk_path = Path.explode(jdk_name)
- val component_dir = dir + jdk_path
+ templates.filterNot(p1 => platforms.exists(p2 => p1.platform_name == p2.platform_name))
+ match {
+ case Nil =>
+ case missing => error("Missing platforms: " + commas_quote(missing.map(_.platform_name)))
+ }
- Isabelle_System.make_directory(component_dir + Path.explode("etc"))
- File.write(Components.settings(component_dir), settings)
- File.write(component_dir + Path.explode("README"), readme(jdk_version))
+ val jdk_name = "jdk-" + jdk_version
+ val jdk_path = Path.explode(jdk_name)
+ val component_dir = dir + jdk_path
- for (platform <- platforms) {
- Isabelle_System.move_file(dir + platform.platform_path, component_dir)
- }
+ Isabelle_System.make_directory(component_dir + Path.explode("etc"))
+ File.write(Components.settings(component_dir), settings)
+ File.write(component_dir + Path.explode("README"), readme(jdk_version))
+
+ for (platform <- platforms) {
+ Isabelle_System.move_file(dir + platform.platform_path, component_dir)
+ }
- for (file <- File.find_files(component_dir.file, include_dirs = true)) {
- val path = file.toPath
- val perms = Files.getPosixFilePermissions(path)
- perms.add(PosixFilePermission.OWNER_READ)
- perms.add(PosixFilePermission.GROUP_READ)
- perms.add(PosixFilePermission.OTHERS_READ)
+ for (file <- File.find_files(component_dir.file, include_dirs = true)) {
+ val path = file.toPath
+ val perms = Files.getPosixFilePermissions(path)
+ perms.add(PosixFilePermission.OWNER_READ)
+ perms.add(PosixFilePermission.GROUP_READ)
+ perms.add(PosixFilePermission.OTHERS_READ)
+ perms.add(PosixFilePermission.OWNER_WRITE)
+ if (file.isDirectory) {
perms.add(PosixFilePermission.OWNER_WRITE)
- if (file.isDirectory) {
- perms.add(PosixFilePermission.OWNER_WRITE)
- perms.add(PosixFilePermission.OWNER_EXECUTE)
- perms.add(PosixFilePermission.GROUP_EXECUTE)
- perms.add(PosixFilePermission.OTHERS_EXECUTE)
- }
- Files.setPosixFilePermissions(path, perms)
+ perms.add(PosixFilePermission.OWNER_EXECUTE)
+ perms.add(PosixFilePermission.GROUP_EXECUTE)
+ perms.add(PosixFilePermission.OTHERS_EXECUTE)
}
+ Files.setPosixFilePermissions(path, perms)
+ }
- progress.echo("Archiving ...")
- Isabelle_System.gnutar(
- "-czf " + File.bash_path(target_dir + jdk_path.tar.gz) + " " + jdk_name, dir = dir).check
- })
+ progress.echo("Archiving ...")
+ Isabelle_System.gnutar(
+ "-czf " + File.bash_path(target_dir + jdk_path.tar.gz) + " " + jdk_name, dir = dir).check
+ }
}
@@ -209,10 +209,11 @@
val isabelle_tool =
Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives",
- Scala_Project.here, args => {
- var target_dir = Path.current
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_jdk [OPTIONS] ARCHIVES...
Options are:
@@ -221,14 +222,14 @@
Build jdk component from tar.gz archives, with original jdk archives
for Linux, Windows, and macOS.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)))
+ "D:" -> (arg => target_dir = Path.explode(arg)))
- val more_args = getopts(args)
- if (more_args.isEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.isEmpty) getopts.usage()
- val archives = more_args.map(Path.explode)
- val progress = new Console_Progress()
+ val archives = more_args.map(Path.explode)
+ val progress = new Console_Progress()
- build_jdk(archives = archives, progress = progress, target_dir = target_dir)
- })
+ build_jdk(archives = archives, progress = progress, target_dir = target_dir)
+ })
}
--- a/src/Pure/Admin/build_jedit.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_jedit.scala Fri Apr 01 23:19:12 2022 +0200
@@ -136,7 +136,7 @@
path
}
- Isabelle_System.with_tmp_dir("tmp")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("tmp") { tmp_dir =>
/* original version */
val install_path = download_jedit(tmp_dir, "install.jar")
@@ -191,7 +191,7 @@
"no_build = true\n" +
"requirements = env:JEDIT_JARS\n" +
("sources =" :: java_sources.sorted.map(" " + _)).mkString("", " \\\n", "\n"))
- })
+ }
/* jars */
@@ -203,13 +203,13 @@
}
for { (name, vers) <- download_plugins } {
- Isabelle_System.with_tmp_file("tmp", ext = "zip")(zip_path => {
+ Isabelle_System.with_tmp_file("tmp", ext = "zip") { zip_path =>
val url =
"https://sourceforge.net/projects/jedit-plugins/files/" + name + "/" + vers + "/" +
name + "-" + vers + "-bin.zip/download"
Isabelle_System.download_file(url, zip_path, progress = progress)
Isabelle_System.bash("unzip -x " + File.bash_path(zip_path), cwd = jars_dir.file).check
- })
+ }
}
@@ -511,13 +511,14 @@
val isabelle_tool =
Isabelle_Tool("build_jedit", "build Isabelle component from the jEdit text-editor",
- Scala_Project.here, args => {
- var target_dir = Path.current
- var java_home = default_java_home
- var original = false
- var version = default_version
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var java_home = default_java_home
+ var original = false
+ var version = default_version
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_jedit [OPTIONS]
Options are:
@@ -528,18 +529,18 @@
Build auxiliary jEdit component from original sources, with some patches.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "J:" -> (arg => java_home = Path.explode(arg)),
- "O" -> (_ => original = true),
- "V:" -> (arg => version = arg))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "J:" -> (arg => java_home = Path.explode(arg)),
+ "O" -> (_ => original = true),
+ "V:" -> (arg => version = arg))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val component_dir = target_dir + Path.basic("jedit-" + Date.Format.alt_date(Date.now()))
- val progress = new Console_Progress()
+ val component_dir = target_dir + Path.basic("jedit-" + Date.Format.alt_date(Date.now()))
+ val progress = new Console_Progress()
- build_jedit(component_dir, version, original = original,
- java_home = java_home, progress = progress)
- })
+ build_jedit(component_dir, version, original = original,
+ java_home = java_home, progress = progress)
+ })
}
--- a/src/Pure/Admin/build_log.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_log.scala Fri Apr 01 23:19:12 2022 +0200
@@ -862,7 +862,7 @@
Isabelle_System.make_directory(sqlite_database.dir)
sqlite_database.file.delete
- using(SQLite.open_database(sqlite_database))(db2 => {
+ using(SQLite.open_database(sqlite_database)) { db2 =>
db.transaction {
db2.transaction {
// main content
@@ -892,9 +892,9 @@
val afp_rev = if (afp) Some("") else None
val table = Data.pull_date_table(afp)
db2.create_table(table)
- db2.using_statement(table.insert())(stmt2 => {
+ db2.using_statement(table.insert()) { stmt2 =>
db.using_statement(
- Data.recent_pull_date_table(days, afp_rev = afp_rev).query)(stmt => {
+ Data.recent_pull_date_table(days, afp_rev = afp_rev).query) { stmt =>
val res = stmt.execute_query()
while (res.next()) {
for ((c, i) <- table.columns.zipWithIndex) {
@@ -902,8 +902,8 @@
}
stmt2.execute()
}
- })
- })
+ }
+ }
}
// full view
@@ -911,7 +911,7 @@
}
}
db2.rebuild
- })
+ }
}
def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
@@ -920,7 +920,7 @@
def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit = {
val table = Data.meta_info_table
- db.using_statement(db.insert_permissive(table))(stmt => {
+ db.using_statement(db.insert_permissive(table)) { stmt =>
stmt.string(1) = log_name
for ((c, i) <- table.columns.tail.zipWithIndex) {
if (c.T == SQL.Type.Date)
@@ -929,12 +929,12 @@
stmt.string(i + 2) = meta_info.get(c)
}
stmt.execute()
- })
+ }
}
def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info): Unit = {
val table = Data.sessions_table
- db.using_statement(db.insert_permissive(table))(stmt => {
+ db.using_statement(db.insert_permissive(table)) { stmt =>
val sessions =
if (build_info.sessions.isEmpty) Build_Info.sessions_dummy
else build_info.sessions
@@ -958,12 +958,12 @@
stmt.string(17) = session.sources
stmt.execute()
}
- })
+ }
}
def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info): Unit = {
val table = Data.theories_table
- db.using_statement(db.insert_permissive(table))(stmt => {
+ db.using_statement(db.insert_permissive(table)) { stmt =>
val sessions =
if (build_info.sessions.forall({ case (_, session) => session.theory_timings.isEmpty }))
Build_Info.sessions_dummy
@@ -980,12 +980,12 @@
stmt.long(6) = timing.gc.ms
stmt.execute()
}
- })
+ }
}
def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info): Unit = {
val table = Data.ml_statistics_table
- db.using_statement(db.insert_permissive(table))(stmt => {
+ db.using_statement(db.insert_permissive(table)) { stmt =>
val ml_stats: List[(String, Option[Bytes])] =
Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
{ case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.xz).proper) },
@@ -997,7 +997,7 @@
stmt.bytes(3) = ml_statistics
stmt.execute()
}
- })
+ }
}
def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false): Unit = {
@@ -1048,7 +1048,7 @@
def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] = {
val table = Data.meta_info_table
val columns = table.columns.tail
- db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt => {
+ db.using_statement(table.select(columns, Data.log_name.where_equal(log_name))) { stmt =>
val res = stmt.execute_query()
if (!res.next()) None
else {
@@ -1063,7 +1063,7 @@
val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
Some(Meta_Info(props, settings))
}
- })
+ }
}
def read_build_info(
@@ -1094,8 +1094,8 @@
else (columns1, table1.ident)
val sessions =
- db.using_statement(SQL.select(columns) + from + " " + where)(stmt => {
- stmt.execute_query().iterator(res => {
+ db.using_statement(SQL.select(columns) + from + " " + where) { stmt =>
+ stmt.execute_query().iterator({ res =>
val session_name = res.string(Data.session_name)
val session_entry =
Session_Entry(
@@ -1116,7 +1116,7 @@
else Nil)
session_name -> session_entry
}).toMap
- })
+ }
Build_Info(sessions)
}
}
--- a/src/Pure/Admin/build_minisat.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_minisat.scala Fri Apr 01 23:19:12 2022 +0200
@@ -22,7 +22,7 @@
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
- Isabelle_System.with_tmp_dir("build")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
@@ -113,7 +113,7 @@
Makarius
""" + Date.Format.date(Date.now()) + "\n")
- })
+ }
}
@@ -121,13 +121,13 @@
val isabelle_tool =
Isabelle_Tool("build_minisat", "build prover component from sources", Scala_Project.here,
- args => {
- var target_dir = Path.current
- var download_url = default_download_url
- var component_name = ""
- var verbose = false
+ { args =>
+ var target_dir = Path.current
+ var download_url = default_download_url
+ var component_name = ""
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_minisat [OPTIONS]
Options are:
@@ -139,17 +139,17 @@
Build prover component from official download.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "U:" -> (arg => download_url = arg),
- "n:" -> (arg => component_name = arg),
- "v" -> (_ => verbose = true))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => download_url = arg),
+ "n:" -> (arg => component_name = arg),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_minisat(download_url = download_url, component_name = component_name,
- verbose = verbose, progress = progress, target_dir = target_dir)
- })
+ build_minisat(download_url = download_url, component_name = component_name,
+ verbose = verbose, progress = progress, target_dir = target_dir)
+ })
}
--- a/src/Pure/Admin/build_pdfjs.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_pdfjs.scala Fri Apr 01 23:19:12 2022 +0200
@@ -38,12 +38,12 @@
/* download */
val download_url = base_url + "/v" + version
- Isabelle_System.with_tmp_file("archive", ext = "zip")(archive_file => {
+ Isabelle_System.with_tmp_file("archive", ext = "zip") { archive_file =>
Isabelle_System.download_file(download_url + "/pdfjs-" + version + "-dist.zip",
archive_file, progress = progress)
Isabelle_System.bash("unzip -x " + File.bash_path(archive_file),
cwd = component_dir.file).check
- })
+ }
/* settings */
@@ -72,12 +72,13 @@
val isabelle_tool =
Isabelle_Tool("build_pdfjs", "build component for Mozilla PDF.js",
- Scala_Project.here, args => {
- var target_dir = Path.current
- var base_url = default_url
- var version = default_version
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var base_url = default_url
+ var version = default_version
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_pdfjs [OPTIONS]
Options are:
@@ -87,16 +88,16 @@
Build component for PDF.js.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "U:" -> (arg => base_url = arg),
- "V:" -> (arg => version = arg))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => base_url = arg),
+ "V:" -> (arg => version = arg))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_pdfjs(base_url = base_url, version = version, target_dir = target_dir,
- progress = progress)
- })
+ build_pdfjs(base_url = base_url, version = version, target_dir = target_dir,
+ progress = progress)
+ })
}
--- a/src/Pure/Admin/build_polyml.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_polyml.scala Fri Apr 01 23:19:12 2022 +0200
@@ -201,12 +201,13 @@
/** Isabelle tool wrappers **/
val isabelle_tool1 =
- Isabelle_Tool("build_polyml", "build Poly/ML from sources", Scala_Project.here, args => {
- var mingw = MinGW.none
- var arch_64 = false
- var sha1_root: Option[Path] = None
+ Isabelle_Tool("build_polyml", "build Poly/ML from sources", Scala_Project.here,
+ { args =>
+ var mingw = MinGW.none
+ var arch_64 = false
+ var sha1_root: Option[Path] = None
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
Options are:
@@ -218,31 +219,32 @@
Build Poly/ML in the ROOT directory of its sources, with additional
CONFIGURE_OPTIONS (e.g. --without-gmp).
""",
- "M:" -> (arg => mingw = MinGW(Path.explode(arg))),
- "m:" ->
- {
- case "32" => arch_64 = false
- case "64" => arch_64 = true
- case bad => error("Bad processor architecture: " + quote(bad))
- },
- "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
+ "M:" -> (arg => mingw = MinGW(Path.explode(arg))),
+ "m:" ->
+ {
+ case "32" => arch_64 = false
+ case "64" => arch_64 = true
+ case bad => error("Bad processor architecture: " + quote(bad))
+ },
+ "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
- val more_args = getopts(args)
- val (root, options) =
- more_args match {
- case root :: options => (Path.explode(root), options)
- case Nil => getopts.usage()
- }
- build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
- arch_64 = arch_64, options = options, mingw = mingw)
- })
+ val more_args = getopts(args)
+ val (root, options) =
+ more_args match {
+ case root :: options => (Path.explode(root), options)
+ case Nil => getopts.usage()
+ }
+ build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
+ arch_64 = arch_64, options = options, mingw = mingw)
+ })
val isabelle_tool2 =
Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component",
- Scala_Project.here, args => {
- var sha1_root: Option[Path] = None
-
- val getopts = Getopts("""
+ Scala_Project.here,
+ { args =>
+ var sha1_root: Option[Path] = None
+
+ val getopts = Getopts("""
Usage: isabelle build_polyml_component [OPTIONS] SOURCE_ARCHIVE COMPONENT_DIR
Options are:
@@ -251,15 +253,15 @@
Make skeleton for Poly/ML component, based on official source archive
(zip or tar.gz).
""",
- "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
+ "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
- val more_args = getopts(args)
+ val more_args = getopts(args)
- val (source_archive, component_dir) =
- more_args match {
- case List(archive, dir) => (Path.explode(archive), Path.explode(dir))
- case _ => getopts.usage()
- }
- build_polyml_component(source_archive, component_dir, sha1_root = sha1_root)
- })
+ val (source_archive, component_dir) =
+ more_args match {
+ case List(archive, dir) => (Path.explode(archive), Path.explode(dir))
+ case _ => getopts.usage()
+ }
+ build_polyml_component(source_archive, component_dir, sha1_root = sha1_root)
+ })
}
--- a/src/Pure/Admin/build_release.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_release.scala Fri Apr 01 23:19:12 2022 +0200
@@ -103,7 +103,7 @@
object Release_Archive {
def make(bytes: Bytes, rename: String = ""): Release_Archive = {
Isabelle_System.with_tmp_dir("tmp")(dir =>
- Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => {
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path =>
val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
Bytes.write(archive_path, bytes)
@@ -122,7 +122,7 @@
(Bytes.read(archive_path), rename)
}
new Release_Archive(bytes1, id, tags, identifier1)
- })
+ }
)
}
@@ -235,9 +235,9 @@
case s => error("Malformed option " + server_option + ": " + quote(s))
}
try {
- Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar => {
+ Isabelle_System.with_tmp_file("tmp", ext = "tar") { local_tmp_tar =>
execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
- ssh.with_tmp_dir(remote_dir => {
+ ssh.with_tmp_dir { remote_dir =>
val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
ssh.write_file(remote_tmp_tar, local_tmp_tar)
val remote_commands =
@@ -248,9 +248,9 @@
"tar -cf tmp.tar heaps")
ssh.execute(remote_commands.mkString(" && "), settings = false).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
- })
+ }
execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
- })
+ }
}
finally { ssh.close() }
}
@@ -496,14 +496,14 @@
Isabelle_System.rm_tree(context.dist_dir + path)
}
- Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => {
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path =>
Bytes.write(archive_path, archive.bytes)
val extract =
List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
map(name => context.dist_name + "/" + name)
execute_tar(context.dist_dir,
"-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract))
- })
+ }
Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE)
@@ -518,7 +518,7 @@
progress.echo("\nApplication bundle for " + platform)
- Isabelle_System.with_tmp_dir("build_release")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("build_release") { tmp_dir =>
// release archive
execute_tar(tmp_dir, "-xzf " + File.bash_path(context.isabelle_archive))
@@ -566,13 +566,13 @@
val base = isabelle_target.absolute
val classpath1 = Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH"))
val classpath2 = Path.split(other_isabelle.getenv("ISABELLE_SETUP_CLASSPATH"))
- (classpath1 ::: classpath2).map(path => {
+ (classpath1 ::: classpath2).map { path =>
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
case None => error("Bad classpath element: " + abs_path)
}
- })
+ }
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
@@ -766,7 +766,7 @@
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
File.set_executable(context.dist_dir + isabelle_exe, true)
}
- })
+ }
progress.echo("DONE")
}
@@ -815,26 +815,26 @@
progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
}
else {
- Isabelle_System.with_tmp_dir("build_release")(tmp_dir => {
- val bundle =
- context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
- execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
+ Isabelle_System.with_tmp_dir("build_release") { tmp_dir =>
+ val bundle =
+ context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
+ execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
- val other_isabelle = context.other_isabelle(tmp_dir)
+ val other_isabelle = context.other_isabelle(tmp_dir)
- Isabelle_System.make_directory(other_isabelle.etc)
- File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\n")
+ Isabelle_System.make_directory(other_isabelle.etc)
+ File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\n")
- other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
- " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
- " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
- other_isabelle.isabelle_home_user.file.delete
+ other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
+ " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
+ " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
+ other_isabelle.isabelle_home_user.file.delete
- execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name))
- execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name))
- execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
- " " + Bash.string(context.dist_name + "/browser_info"))
- })
+ execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name))
+ execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name))
+ execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
+ " " + Bash.string(context.dist_name + "/browser_info"))
+ }
}
}
}
--- a/src/Pure/Admin/build_scala.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_scala.scala Fri Apr 01 23:19:12 2022 +0200
@@ -29,12 +29,12 @@
Isabelle_System.download_file(proper_url, path, progress = progress)
def get_unpacked(dir: Path, strip: Int = 0, progress: Progress = new Progress): Unit =
- Isabelle_System.with_tmp_file("archive")(archive_path => {
+ Isabelle_System.with_tmp_file("archive"){ archive_path =>
get(archive_path, progress = progress)
progress.echo("Unpacking " + artifact)
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
- dir = dir, strip = strip).check
- })
+ Isabelle_System.gnutar(
+ "-xzf " + File.bash_path(archive_path), dir = dir, strip = strip).check
+ }
def print: String =
" * " + name + " " + version +
@@ -139,10 +139,11 @@
val isabelle_tool =
Isabelle_Tool("build_scala", "build Isabelle Scala component from official downloads",
- Scala_Project.here, args => {
- var target_dir = Path.current
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_scala [OPTIONS]
Options are:
@@ -150,13 +151,13 @@
Build Isabelle Scala component from official downloads.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)))
+ "D:" -> (arg => target_dir = Path.explode(arg)))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_scala(target_dir = target_dir, progress = progress)
- })
+ build_scala(target_dir = target_dir, progress = progress)
+ })
}
--- a/src/Pure/Admin/build_spass.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_spass.scala Fri Apr 01 23:19:12 2022 +0200
@@ -18,7 +18,7 @@
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current): Unit = {
- Isabelle_System.with_tmp_dir("build")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("build") { tmp_dir =>
Isabelle_System.require_command("bison")
Isabelle_System.require_command("flex")
@@ -140,19 +140,20 @@
Makarius
""" + Date.Format.date(Date.now()) + "\n")
- })
+ }
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_spass", "build prover component from source distribution",
- Scala_Project.here, args => {
- var target_dir = Path.current
- var download_url = default_download_url
- var verbose = false
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var download_url = default_download_url
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_spass [OPTIONS]
Options are:
@@ -163,16 +164,16 @@
Build prover component from the specified source distribution.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "U:" -> (arg => download_url = arg),
- "v" -> (_ => verbose = true))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => download_url = arg),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_spass(download_url = download_url, verbose = verbose, progress = progress,
- target_dir = target_dir)
- })
+ build_spass(download_url = download_url, verbose = verbose, progress = progress,
+ target_dir = target_dir)
+ })
}
--- a/src/Pure/Admin/build_sqlite.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_sqlite.scala Fri Apr 01 23:19:12 2022 +0200
@@ -54,7 +54,7 @@
val jar = component_dir + Path.basic(download_name).ext("jar")
Isabelle_System.download_file(download_url, jar, progress = progress)
- Isabelle_System.with_tmp_dir("sqlite")(jar_dir => {
+ Isabelle_System.with_tmp_dir("sqlite") { jar_dir =>
progress.echo("Unpacking " + jar)
Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute),
cwd = jar_dir.file).check
@@ -75,7 +75,7 @@
}
File.set_executable(component_dir + Path.explode("x86_64-windows/sqlitejdbc.dll"), true)
- })
+ }
}
@@ -83,10 +83,11 @@
val isabelle_tool =
Isabelle_Tool("build_sqlite", "build Isabelle sqlite-jdbc component from official download",
- Scala_Project.here, args => {
- var target_dir = Path.current
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_sqlite [OPTIONS] DOWNLOAD
Options are:
@@ -96,17 +97,17 @@
https://github.com/xerial/sqlite-jdbc and
https://oss.sonatype.org/content/repositories/releases/org/xerial/sqlite-jdbc
""",
- "D:" -> (arg => target_dir = Path.explode(arg)))
+ "D:" -> (arg => target_dir = Path.explode(arg)))
- val more_args = getopts(args)
- val download_url =
- more_args match {
- case List(download_url) => download_url
- case _ => getopts.usage()
- }
+ val more_args = getopts(args)
+ val download_url =
+ more_args match {
+ case List(download_url) => download_url
+ case _ => getopts.usage()
+ }
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_sqlite(download_url, progress = progress, target_dir = target_dir)
- })
+ build_sqlite(download_url, progress = progress, target_dir = target_dir)
+ })
}
--- a/src/Pure/Admin/build_status.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_status.scala Fri Apr 01 23:19:12 2022 +0200
@@ -228,7 +228,7 @@
val store = Build_Log.store(options)
- using(store.open_database())(db => {
+ using(store.open_database()) { db =>
for (profile <- profiles.sortBy(_.description)) {
progress.echo("input " + quote(profile.description))
@@ -262,7 +262,7 @@
val sql = profile.select(options, columns, only_sessions)
progress.echo_if(verbose, sql)
- db.using_statement(sql)(stmt => {
+ db.using_statement(sql) { stmt =>
val res = stmt.execute_query()
while (res.next()) {
val session_name = res.string(Build_Log.Data.session_name)
@@ -349,9 +349,9 @@
data_entries += (data_name -> (sessions + (session_name -> session)))
}
}
- })
+ }
}
- })
+ }
val sorted_entries =
(for {
@@ -582,15 +582,16 @@
val isabelle_tool =
Isabelle_Tool("build_status", "present recent build status information from database",
- Scala_Project.here, args => {
- var target_dir = default_target_dir
- var ml_statistics = false
- var only_sessions = Set.empty[String]
- var options = Options.init()
- var image_size = default_image_size
- var verbose = false
+ Scala_Project.here,
+ { args =>
+ var target_dir = default_target_dir
+ var ml_statistics = false
+ var only_sessions = Set.empty[String]
+ var options = Options.init()
+ var image_size = default_image_size
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_status [OPTIONS]
Options are:
@@ -606,24 +607,24 @@
via system options build_log_database_host, build_log_database_user,
build_log_history etc.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "M" -> (_ => ml_statistics = true),
- "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
- "l:" -> (arg => options = options + ("build_log_history=" + arg)),
- "o:" -> (arg => options = options + arg),
- "s:" -> (arg =>
- space_explode('x', arg).map(Value.Int.parse) match {
- case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
- case _ => error("Error bad PNG image size: " + quote(arg))
- }),
- "v" -> (_ => verbose = true))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "M" -> (_ => ml_statistics = true),
+ "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
+ "l:" -> (arg => options = options + ("build_log_history=" + arg)),
+ "o:" -> (arg => options = options + arg),
+ "s:" -> (arg =>
+ space_explode('x', arg).map(Value.Int.parse) match {
+ case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
+ case _ => error("Error bad PNG image size: " + quote(arg))
+ }),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress
+ val progress = new Console_Progress
- build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose,
- target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size)
- })
+ build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose,
+ target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size)
+ })
}
--- a/src/Pure/Admin/build_vampire.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_vampire.scala Fri Apr 01 23:19:12 2022 +0200
@@ -27,7 +27,7 @@
): Unit = {
Isabelle_System.require_command("cmake")
- Isabelle_System.with_tmp_dir("build")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
@@ -118,7 +118,7 @@
Makarius
""" + Date.Format.date(Date.now()) + "\n")
- })
+ }
}
@@ -126,7 +126,8 @@
val isabelle_tool =
Isabelle_Tool("build_vampire", "build prover component from official download",
- Scala_Project.here, args => {
+ Scala_Project.here,
+ { args =>
var target_dir = Path.current
var download_url = default_download_url
var jobs = default_jobs
--- a/src/Pure/Admin/build_verit.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_verit.scala Fri Apr 01 23:19:12 2022 +0200
@@ -22,7 +22,7 @@
): Unit = {
mingw.check
- Isabelle_System.with_tmp_dir("build")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
val Archive_Name = """^.*?([^/]+)$""".r
@@ -114,7 +114,7 @@
Makarius
""" + Date.Format.date(Date.now()) + "\n")
- })
+ }
}
@@ -122,13 +122,14 @@
val isabelle_tool =
Isabelle_Tool("build_verit", "build prover component from official download",
- Scala_Project.here, args => {
- var target_dir = Path.current
- var mingw = MinGW.none
- var download_url = default_download_url
- var verbose = false
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var mingw = MinGW.none
+ var download_url = default_download_url
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_verit [OPTIONS]
Options are:
@@ -140,17 +141,17 @@
Build prover component from official download.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "M:" -> (arg => mingw = MinGW(Path.explode(arg))),
- "U:" -> (arg => download_url = arg),
- "v" -> (_ => verbose = true))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "M:" -> (arg => mingw = MinGW(Path.explode(arg))),
+ "U:" -> (arg => download_url = arg),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_verit(download_url = download_url, verbose = verbose, progress = progress,
- target_dir = target_dir, mingw = mingw)
- })
+ build_verit(download_url = download_url, verbose = verbose, progress = progress,
+ target_dir = target_dir, mingw = mingw)
+ })
}
--- a/src/Pure/Admin/build_zipperposition.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/build_zipperposition.scala Fri Apr 01 23:19:12 2022 +0200
@@ -19,7 +19,7 @@
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
- Isabelle_System.with_tmp_dir("build")(build_dir => {
+ Isabelle_System.with_tmp_dir("build") { build_dir =>
if (Platform.is_linux) Isabelle_System.require_command("patchelf")
@@ -83,7 +83,7 @@
Makarius
""" + Date.Format.date(Date.now()) + "\n")
- })
+ }
}
@@ -91,12 +91,13 @@
val isabelle_tool =
Isabelle_Tool("build_zipperposition", "build prover component from OPAM repository",
- Scala_Project.here, args => {
- var target_dir = Path.current
- var version = default_version
- var verbose = false
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var version = default_version
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_zipperposition [OPTIONS]
Options are:
@@ -106,16 +107,16 @@
Build prover component from OPAM repository.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "V:" -> (arg => version = arg),
- "v" -> (_ => verbose = true))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "V:" -> (arg => version = arg),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_zipperposition(version = version, verbose = verbose, progress = progress,
- target_dir = target_dir)
- })
+ build_zipperposition(version = version, verbose = verbose, progress = progress,
+ target_dir = target_dir)
+ })
}
--- a/src/Pure/Admin/check_sources.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/check_sources.scala Fri Apr 01 23:19:12 2022 +0200
@@ -59,16 +59,17 @@
val isabelle_tool =
Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources",
- Scala_Project.here, args => {
- val getopts = Getopts("""
+ Scala_Project.here,
+ { args =>
+ val getopts = Getopts("""
Usage: isabelle check_sources [ROOT_DIRS...]
Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS.
""")
- val specs = getopts(args)
- if (specs.isEmpty) getopts.usage()
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
- for (root <- specs) check_hg(Path.explode(root))
- })
+ for (root <- specs) check_hg(Path.explode(root))
+ })
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Apr 01 23:19:12 2022 +0200
@@ -42,7 +42,8 @@
def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
val init: Logger_Task =
- Logger_Task("init", logger => {
+ Logger_Task("init",
+ { logger =>
Isabelle_Devel.make_index()
Mercurial.setup_repository(Isabelle_System.isabelle_repository.root, isabelle_repos)
@@ -60,7 +61,8 @@
})
val exit: Logger_Task =
- Logger_Task("exit", logger => {
+ Logger_Task("exit",
+ { logger =>
Isabelle_System.bash(
"rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.")
.check
@@ -70,7 +72,8 @@
/* Mailman archives */
val mailman_archives: Logger_Task =
- Logger_Task("mailman_archives", logger => {
+ Logger_Task("mailman_archives",
+ { logger =>
Mailman.Isabelle_Users.download(mailman_archives_dir)
Mailman.Isabelle_Dev.download(mailman_archives_dir)
})
@@ -79,9 +82,8 @@
/* build release */
val build_release: Logger_Task =
- Logger_Task("build_release", logger => {
- Isabelle_Devel.release_snapshot(logger.options, get_rev(), get_afp_rev())
- })
+ Logger_Task("build_release",
+ { logger => Isabelle_Devel.release_snapshot(logger.options, get_rev(), get_afp_rev()) })
/* remote build_history */
@@ -113,7 +115,7 @@
days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
db.using_statement(select)(stmt =>
- stmt.execute_query().iterator(res => {
+ stmt.execute_query().iterator({ res =>
val known = res.bool(Build_Log.Data.known)
val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
@@ -170,7 +172,7 @@
val afp_rev = if (afp) Some(get_afp_rev()) else None
val store = Build_Log.store(options)
- using(store.open_database())(db => {
+ using(store.open_database()) { db =>
def pick_days(days: Int, gap: Int): Option[(String, Option[String])] = {
val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
def runs = unknown_runs(items).filter(run => run.length >= gap)
@@ -190,7 +192,7 @@
pick_days(options.int("build_log_history") max history, 2) orElse
pick_days(200, 5) orElse
pick_days(2000, 1)
- })
+ }
}
def build_history_options: String =
@@ -401,28 +403,29 @@
r: Remote_Build
) : Logger_Task = {
val task_name = "build_history-" + r.host
- Logger_Task(task_name, logger => {
- using(r.ssh_session(logger.ssh_context))(ssh => {
- val results =
- Build_History.remote_build_history(ssh,
- isabelle_repos,
- isabelle_repos.ext(r.host),
- isabelle_identifier = "cronjob_build_history",
- self_update = r.self_update,
- rev = rev,
- afp_rev = afp_rev,
- options =
- " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
- " -R " + Bash.string(Components.default_component_repository) +
- " -C '$USER_HOME/.isabelle/contrib' -f " +
- r.build_history_options,
- args = "-o timeout=10800 " + r.args)
+ Logger_Task(task_name,
+ { logger =>
+ using(r.ssh_session(logger.ssh_context)) { ssh =>
+ val results =
+ Build_History.remote_build_history(ssh,
+ isabelle_repos,
+ isabelle_repos.ext(r.host),
+ isabelle_identifier = "cronjob_build_history",
+ self_update = r.self_update,
+ rev = rev,
+ afp_rev = afp_rev,
+ options =
+ " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
+ " -R " + Bash.string(Components.default_component_repository) +
+ " -C '$USER_HOME/.isabelle/contrib' -f " +
+ r.build_history_options,
+ args = "-o timeout=10800 " + r.args)
- for ((log_name, bytes) <- results) {
- logger.log(Date.now(), log_name)
- Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
- }
- })
+ for ((log_name, bytes) <- results) {
+ logger.log(Date.now(), log_name)
+ Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
+ }
+ }
})
}
@@ -443,7 +446,8 @@
private val thread: Consumer_Thread[String] =
Consumer_Thread.fork("cronjob: logger", daemon = true)(
- consume = (text: String) => {
+ consume =
+ { (text: String) =>
// critical
File.append(current_log, text + "\n")
File.append(cumulative_log, text + "\n")
@@ -544,20 +548,22 @@
for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
run_now(task))
- def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ => {
- @tailrec def join(running: List[Task]): Unit = {
- running.partition(_.is_finished) match {
- case (Nil, Nil) =>
- case (Nil, _ :: _) => Time.seconds(0.5).sleep(); join(running)
- case (_ :: _, remaining) => join(remaining)
+ def PAR(tasks: List[Logger_Task]): Logger_Task =
+ Logger_Task(body =
+ { _ =>
+ @tailrec def join(running: List[Task]): Unit = {
+ running.partition(_.is_finished) match {
+ case (Nil, Nil) =>
+ case (Nil, _ :: _) => Time.seconds(0.5).sleep(); join(running)
+ case (_ :: _, remaining) => join(remaining)
+ }
}
- }
- val start_date = Date.now()
- val running =
- for (task <- tasks if !exclude_task(task.name))
- yield log_service.fork_task(start_date, task)
- join(running)
- })
+ val start_date = Date.now()
+ val running =
+ for (task <- tasks if !exclude_task(task.name))
+ yield log_service.fork_task(start_date, task)
+ join(running)
+ })
/* repository structure */
--- a/src/Pure/Admin/isabelle_devel.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala Fri Apr 01 23:19:12 2022 +0200
@@ -33,16 +33,17 @@
/* release snapshot */
def release_snapshot(options: Options, rev: String, afp_rev: String): Unit = {
- Isabelle_System.with_tmp_dir("isadist")(target_dir => {
- Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
- website_dir => {
+ Isabelle_System.with_tmp_dir("isadist") { target_dir =>
+ Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
+ { website_dir =>
val context = Build_Release.Release_Context(target_dir)
Build_Release.build_release_archive(context, rev)
Build_Release.build_release(options, context, afp_rev = afp_rev,
build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
website = Some(website_dir))
- })
- })
+ }
+ )
+ }
}
@@ -50,11 +51,11 @@
def build_log_database(options: Options, log_dirs: List[Path]): Unit = {
val store = Build_Log.store(options)
- using(store.open_database())(db => {
+ using(store.open_database()) { db =>
store.update_database(db, log_dirs)
store.update_database(db, log_dirs, ml_statistics = true)
store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB))
- })
+ }
}
--- a/src/Pure/General/completion.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/completion.scala Fri Apr 01 23:19:12 2022 +0200
@@ -347,7 +347,7 @@
def add_symbols: Completion = {
val words =
- Symbol.symbols.entries.flatMap(entry => {
+ Symbol.symbols.entries.flatMap { entry =>
val sym = entry.symbol
val word = "\\" + entry.name
val seps =
@@ -358,7 +358,7 @@
}
List(sym -> sym, word -> sym) :::
seps.map(sep => word -> (sym + sep + "\\<open>\u0007\\<close>"))
- })
+ }
new Completion(
keywords,
--- a/src/Pure/General/date.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/date.scala Fri Apr 01 23:19:12 2022 +0200
@@ -50,10 +50,10 @@
def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat)
def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
- pats.flatMap(pat => {
+ pats.flatMap { pat =>
val fmt = pattern(pat)
if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale)
- })
+ }
@tailrec def try_variants(
fmts: List[DateTimeFormatter],
--- a/src/Pure/General/file_watcher.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/file_watcher.scala Fri Apr 01 23:19:12 2022 +0200
@@ -91,25 +91,25 @@
while (true) {
val key = watcher.take
val has_changed =
- state.change_result(st => {
- val (remove, changed) =
- st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
- case Some(dir) =>
- val events: Iterable[WatchEvent[JPath]] =
- key.pollEvents.asInstanceOf[JList[WatchEvent[JPath]]].asScala
- val remove = if (key.reset) None else Some(dir)
- val changed =
- events.iterator.foldLeft(Set.empty[JFile]) {
- case (set, event) => set + dir.toPath.resolve(event.context).toFile
- }
- (remove, changed)
- case None =>
- key.pollEvents
- key.reset
- (None, Set.empty[JFile])
- }
- (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
- })
+ state.change_result { st =>
+ val (remove, changed) =
+ st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
+ case Some(dir) =>
+ val events: Iterable[WatchEvent[JPath]] =
+ key.pollEvents.asInstanceOf[JList[WatchEvent[JPath]]].asScala
+ val remove = if (key.reset) None else Some(dir)
+ val changed =
+ events.iterator.foldLeft(Set.empty[JFile]) {
+ case (set, event) => set + dir.toPath.resolve(event.context).toFile
+ }
+ (remove, changed)
+ case None =>
+ key.pollEvents
+ key.reset
+ (None, Set.empty[JFile])
+ }
+ (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
+ }
if (has_changed) delay_changed.invoke()
}
}
--- a/src/Pure/General/graph.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/graph.scala Fri Apr 01 23:19:12 2022 +0200
@@ -52,14 +52,14 @@
/* XML data representation */
def encode[Key, A](key: XML.Encode.T[Key], info: XML.Encode.T[A]): XML.Encode.T[Graph[Key, A]] =
- (graph: Graph[Key, A]) => {
+ { (graph: Graph[Key, A]) =>
import XML.Encode._
list(pair(pair(key, info), list(key)))(graph.dest)
}
def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(
implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] =
- (body: XML.Body) => {
+ { (body: XML.Body) =>
import XML.Decode._
make(list(pair(pair(key, info), list(key)))(body))(ord)
}
--- a/src/Pure/General/graphics_file.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/graphics_file.scala Fri Apr 01 23:19:12 2022 +0200
@@ -60,7 +60,7 @@
def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int): Unit = {
import com.lowagie.text.{Document, Rectangle}
- using(new BufferedOutputStream(new FileOutputStream(file)))(out => {
+ using(new BufferedOutputStream(new FileOutputStream(file))) { out =>
val document = new Document()
try {
document.setPageSize(new Rectangle(width.toFloat, height.toFloat))
@@ -77,7 +77,7 @@
cb.addTemplate(tp, 1, 0, 0, 1, 0, 0)
}
finally { document.close() }
- })
+ }
}
--- a/src/Pure/General/http.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/http.scala Fri Apr 01 23:19:12 2022 +0200
@@ -84,7 +84,7 @@
val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r
val start = Time.now()
- using(connection.getInputStream)(stream => {
+ using(connection.getInputStream) { stream =>
val bytes = Bytes.read_stream(stream, hint = connection.getContentLength)
val stop = Time.now()
@@ -98,7 +98,7 @@
}
Content(bytes, file_name = file_name, mime_type = mime_type,
encoding = encoding, elapsed_time = stop - start)
- })
+ }
}
def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content =
@@ -118,7 +118,7 @@
connection.setRequestProperty(
"Content-Type", "multipart/form-data; boundary=" + quote(boundary))
- using(connection.getOutputStream)(out => {
+ using(connection.getOutputStream) { out =>
def output(s: String): Unit = out.write(UTF8.bytes(s))
def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE))
def output_boundary(end: Boolean = false): Unit =
@@ -152,7 +152,7 @@
}
output_boundary(end = true)
out.flush()
- })
+ }
get_content(connection)
}
@@ -238,7 +238,7 @@
def context(server_name: String): String =
proper_string(url_path(server_name, name)).getOrElse("/")
- def handler(server_name: String): HttpHandler = (http: HttpExchange) => {
+ def handler(server_name: String): HttpHandler = { (http: HttpExchange) =>
val uri = http.getRequestURI
val input = using(http.getRequestBody)(Bytes.read_stream(_))
if (http.getRequestMethod == method) {
--- a/src/Pure/General/mercurial.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/mercurial.scala Fri Apr 01 23:19:12 2022 +0200
@@ -68,13 +68,13 @@
def download_dir(dir: Path, rev: String = "tip", progress: Progress = new Progress): Unit = {
Isabelle_System.new_directory(dir)
- Isabelle_System.with_tmp_file("rev", ext = ".tar.gz")(archive_path => {
+ Isabelle_System.with_tmp_file("rev", ext = ".tar.gz") { archive_path =>
val content = download_archive(rev = rev, progress = progress)
Bytes.write(archive_path, content.bytes)
progress.echo("Unpacking " + rev + ".tar.gz")
Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
dir = dir, original_owner = true, strip = 1).check
- })
+ }
}
}
@@ -397,12 +397,13 @@
val isabelle_tool =
Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository",
- Scala_Project.here, args => {
- var remote_name = ""
- var path_name = default_path_name
- var remote_exists = false
+ Scala_Project.here,
+ { args =>
+ var remote_name = ""
+ var path_name = default_path_name
+ var remote_exists = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
Options are:
@@ -413,21 +414,21 @@
Setup a remote vs. local Mercurial repository: REMOTE either refers to a
Phabricator server "user@host" or SSH file server "ssh://user@host/path".
""",
- "n:" -> (arg => remote_name = arg),
- "p:" -> (arg => path_name = arg),
- "r" -> (_ => remote_exists = true))
+ "n:" -> (arg => remote_name = arg),
+ "p:" -> (arg => path_name = arg),
+ "r" -> (_ => remote_exists = true))
- val more_args = getopts(args)
+ val more_args = getopts(args)
- val (remote, local_path) =
- more_args match {
- case List(arg1, arg2) => (arg1, Path.explode(arg2))
- case _ => getopts.usage()
- }
+ val (remote, local_path) =
+ more_args match {
+ case List(arg1, arg2) => (arg1, Path.explode(arg2))
+ case _ => getopts.usage()
+ }
- val progress = new Console_Progress
+ val progress = new Console_Progress
- hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name,
- remote_exists = remote_exists, progress = progress)
- })
+ hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name,
+ remote_exists = remote_exists, progress = progress)
+ })
}
--- a/src/Pure/General/scan.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/scan.scala Fri Apr 01 23:19:12 2022 +0200
@@ -398,18 +398,18 @@
private def make_byte_reader(stream: InputStream, stream_length: Int): Byte_Reader = {
val buffered_stream = new BufferedInputStream(stream)
- val seq = new PagedSeq(
- (buf: Array[Char], offset: Int, length: Int) => {
- var i = 0
- var c = 0
- var eof = false
- while (!eof && i < length) {
- c = buffered_stream.read
- if (c == -1) eof = true
- else { buf(offset + i) = c.toChar; i += 1 }
- }
- if (i > 0) i else -1
- })
+ val seq =
+ new PagedSeq({ (buf: Array[Char], offset: Int, length: Int) =>
+ var i = 0
+ var c = 0
+ var eof = false
+ while (!eof && i < length) {
+ c = buffered_stream.read
+ if (c == -1) eof = true
+ else { buf(offset + i) = c.toChar; i += 1 }
+ }
+ if (i > 0) i else -1
+ })
val restricted_seq = new Restricted_Seq(seq, 0, stream_length)
class Paged_Reader(override val offset: Int) extends Byte_Reader {
--- a/src/Pure/General/sha1.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/sha1.scala Fri Apr 01 23:19:12 2022 +0200
@@ -33,16 +33,16 @@
}
def digest(file: JFile): Digest =
- make_digest(sha => using(new FileInputStream(file))(stream => {
- val buf = new Array[Byte](65536)
- var m = 0
- var cont = true
- while (cont) {
- m = stream.read(buf, 0, buf.length)
- if (m != -1) sha.update(buf, 0, m)
- cont = (m != -1)
- }
- }))
+ make_digest(sha => using(new FileInputStream(file)) { stream =>
+ val buf = new Array[Byte](65536)
+ var m = 0
+ var cont = true
+ while (cont) {
+ m = stream.read(buf, 0, buf.length)
+ if (m != -1) sha.update(buf, 0, m)
+ cont = (m != -1)
+ }
+ })
def digest(path: Path): Digest = digest(path.file)
def digest(bytes: Array[Byte]): Digest = make_digest(_.update(bytes))
--- a/src/Pure/General/ssh.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/General/ssh.scala Fri Apr 01 23:19:12 2022 +0200
@@ -152,7 +152,7 @@
connect_session(host = fw.local_host, port = fw.local_port,
host_key_permissive = permissive,
nominal_host = host, nominal_user = user, user = user,
- on_close = () => { fw.close(); proxy.close() })
+ on_close = { () => fw.close(); proxy.close() })
}
catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
}
--- a/src/Pure/ML/ml_process.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/ML/ml_process.scala Fri Apr 01 23:19:12 2022 +0200
@@ -129,26 +129,27 @@
cwd = cwd,
env = bash_env,
redirect = redirect,
- cleanup = () => {
- isabelle_process_options.delete
- init_session.delete
- Isabelle_System.rm_tree(isabelle_tmp)
- cleanup()
- })
+ cleanup = { () =>
+ isabelle_process_options.delete
+ init_session.delete
+ Isabelle_System.rm_tree(isabelle_tmp)
+ cleanup()
+ })
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)",
- Scala_Project.here, 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()
+ Scala_Project.here,
+ { 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("""
+ val getopts = Getopts("""
Usage: isabelle process [OPTIONS]
Options are:
@@ -162,27 +163,26 @@
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))
+ "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.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (args.isEmpty || more_args.nonEmpty) getopts.usage()
- val base_info = Sessions.base_info(options, logic, dirs = dirs).check
- val store = Sessions.store(options)
- val result =
- ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args,
- modes = modes, session_base = Some(base_info.base))
- .result(
- progress_stdout = Output.writeln(_, stdout = true),
- progress_stderr = Output.writeln(_))
+ val base_info = Sessions.base_info(options, logic, dirs = dirs).check
+ val store = Sessions.store(options)
+ val result =
+ ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args,
+ modes = modes, session_base = Some(base_info.base)).result(
+ progress_stdout = Output.writeln(_, stdout = true),
+ progress_stderr = Output.writeln(_))
- sys.exit(result.rc)
- })
+ sys.exit(result.rc)
+ })
}
--- a/src/Pure/PIDE/document.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/PIDE/document.scala Fri Apr 01 23:19:12 2022 +0200
@@ -679,7 +679,7 @@
def command_results(range: Text.Range): Command.Results =
Command.State.merge_results(
select[List[Command.State]](range, Markup.Elements.full,
- command_states => { case _ => Some(command_states) }).flatMap(_.info))
+ command_states => _ => Some(command_states)).flatMap(_.info))
def command_results(command: Command): Command.Results =
state.command_results(version, command)
--- a/src/Pure/PIDE/headless.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/PIDE/headless.scala Fri Apr 01 23:19:12 2022 +0200
@@ -321,7 +321,7 @@
val version = snapshot.version
val theory_progress =
- use_theories_state.change_result(st => {
+ use_theories_state.change_result { st =>
val domain =
if (st.nodes_status.is_empty) dep_theories_set
else changed.nodes.iterator.filter(dep_theories_set).toSet
@@ -343,7 +343,7 @@
} yield Progress.Theory(name.theory, percentage = Some(p1))).toList
(theory_progress, st.update(nodes_status1))
- })
+ }
theory_progress.foreach(progress.theory)
@@ -451,7 +451,7 @@
def update_blobs(names: List[Document.Node.Name]): (Document.Blobs, State) = {
val new_blobs =
- names.flatMap(name => {
+ names.flatMap { name =>
val bytes = Bytes.read(name.path)
def new_blob: Document.Blob = {
val text = bytes.text
@@ -461,7 +461,7 @@
case Some(blob) => if (blob.bytes == bytes) None else Some(name -> new_blob)
case None => Some(name -> new_blob)
}
- })
+ }
val blobs1 = new_blobs.foldLeft(blobs)(_ + _)
val blobs2 = new_blobs.foldLeft(blobs) { case (map, (a, b)) => map + (a -> b.unchanged) }
(Document.Blobs(blobs1), copy(blobs = blobs2))
@@ -601,7 +601,7 @@
val loaded = loaded_theories.length
if (loaded > 1) progress.echo("Loading " + loaded + " theories ...")
- state.change(st => {
+ state.change { st =>
val (doc_blobs1, st1) = st.insert_required(id, theories).update_blobs(files)
val theory_edits =
for (theory <- loaded_theories)
@@ -617,34 +617,34 @@
session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten)
st1.update_theories(theory_edits.map(_._2))
- })
+ }
}
def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]): Unit = {
- state.change(st => {
+ state.change { st =>
val (edits, st1) = st.unload_theories(session, id, theories)
session.update(st.doc_blobs, edits)
st1
- })
+ }
}
def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]): Unit = {
- state.change(st => {
+ state.change { st =>
val (edits1, st1) = st.unload_theories(session, id, theories)
val ((_, _, edits2), st2) = st1.purge_theories(session, None)
session.update(st.doc_blobs, edits1 ::: edits2)
st2
- })
+ }
}
def purge_theories(
session: Session,
nodes: Option[List[Document.Node.Name]]
) : (List[Document.Node.Name], List[Document.Node.Name]) = {
- state.change_result(st => {
+ state.change_result { st =>
val ((purged, retained, _), st1) = st.purge_theories(session, nodes)
((purged, retained), st1)
- })
+ }
}
}
}
--- a/src/Pure/PIDE/markup.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/PIDE/markup.scala Fri Apr 01 23:19:12 2022 +0200
@@ -730,12 +730,12 @@
/* XML data representation */
- def encode: XML.Encode.T[Markup] = (markup: Markup) => {
+ def encode: XML.Encode.T[Markup] = { (markup: Markup) =>
import XML.Encode._
pair(string, properties)((markup.name, markup.properties))
}
- def decode: XML.Decode.T[Markup] = (body: XML.Body) => {
+ def decode: XML.Decode.T[Markup] = { (body: XML.Body) =>
import XML.Decode._
val (name, props) = pair(string, properties)(body)
Markup(name, props)
--- a/src/Pure/PIDE/protocol.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/PIDE/protocol.scala Fri Apr 01 23:19:12 2022 +0200
@@ -357,9 +357,9 @@
toks_yxml :: toks_sources)
}
- def define_commands(resources: Resources, commands: List[Command]): Unit = {
+ def define_commands(resources: Resources, commands: List[Command]): Unit =
protocol_command_args("Document.define_commands",
- commands.map(command => {
+ commands.map { command =>
import XML.Encode._
val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) =
encode_command(resources, command)
@@ -367,8 +367,7 @@
pair(string, pair(string, pair(string, pair(string, pair(string, list(string))))))(
command_id, (name, (parents_yxml, (blobs_yxml, (toks_yxml, toks_sources)))))
YXML.string_of_body(body)
- }))
- }
+ })
def define_commands_bulk(resources: Resources, commands: List[Command]): Unit = {
val (irregular, regular) = commands.partition(command => YXML.detect(command.source))
--- a/src/Pure/System/components.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/System/components.scala Fri Apr 01 23:19:12 2022 +0200
@@ -223,7 +223,7 @@
if ((publish && archives.nonEmpty) || update_components_sha1) {
options.string("isabelle_components_server") match {
case SSH.Target(user, host) =>
- using(SSH.open_session(options, host = host, user = user))(ssh => {
+ using(SSH.open_session(options, host = host, user = user)) { ssh =>
val components_dir = Path.explode(options.string("isabelle_components_dir"))
val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
@@ -247,10 +247,10 @@
// contrib directory
val is_standard_component =
- Isabelle_System.with_tmp_dir("component")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("component") { tmp_dir =>
Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
check_dir(tmp_dir + Path.explode(name))
- })
+ }
if (is_standard_component) {
if (ssh.is_dir(remote_contrib)) {
if (force) ssh.rm_tree(remote_contrib)
@@ -280,7 +280,7 @@
}
write_components_sha1(read_components_sha1(lines))
}
- })
+ }
case s => error("Bad isabelle_components_server: " + quote(s))
}
}
@@ -310,16 +310,17 @@
val isabelle_tool =
Isabelle_Tool("build_components", "build and publish Isabelle components",
- Scala_Project.here, args => {
- var publish = false
- var update_components_sha1 = false
- var force = false
- var options = Options.init()
+ Scala_Project.here,
+ { args =>
+ var publish = false
+ var update_components_sha1 = false
+ var force = false
+ var options = Options.init()
- def show_options: String =
- cat_lines(relevant_options.map(name => options.options(name).print))
+ def show_options: String =
+ cat_lines(relevant_options.map(name => options.options(name).print))
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS...
Options are:
@@ -332,17 +333,17 @@
depending on system options:
""" + Library.indent_lines(2, show_options) + "\n",
- "P" -> (_ => publish = true),
- "f" -> (_ => force = true),
- "o:" -> (arg => options = options + arg),
- "u" -> (_ => update_components_sha1 = true))
+ "P" -> (_ => publish = true),
+ "f" -> (_ => force = true),
+ "o:" -> (arg => options = options + arg),
+ "u" -> (_ => update_components_sha1 = true))
- val more_args = getopts(args)
- if (more_args.isEmpty && !update_components_sha1) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.isEmpty && !update_components_sha1) getopts.usage()
- val progress = new Console_Progress
+ val progress = new Console_Progress
- build_components(options, more_args.map(Path.explode), progress = progress,
- publish = publish, force = force, update_components_sha1 = update_components_sha1)
- })
+ build_components(options, more_args.map(Path.explode), progress = progress,
+ publish = publish, force = force, update_components_sha1 = update_components_sha1)
+ })
}
--- a/src/Pure/System/isabelle_system.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala Fri Apr 01 23:19:12 2022 +0200
@@ -418,13 +418,13 @@
}
def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
- with_tmp_file("patch")(patch => {
+ with_tmp_file("patch") { patch =>
Isabelle_System.bash(
"diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) +
" > " + File.bash_path(patch),
cwd = base_dir.file).check_rc(_ <= 1)
File.read(patch)
- })
+ }
}
def hostname(): String = bash("hostname -s").check.out
--- a/src/Pure/System/isabelle_tool.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala Fri Apr 01 23:19:12 2022 +0200
@@ -67,16 +67,17 @@
}
private def find_external(name: String): Option[List[String] => Unit] =
- dirs().collectFirst({
- case dir if is_external(dir, name + ".scala") =>
- compile(dir + Path.explode(name + ".scala"))
- case dir if is_external(dir, name) =>
- (args: List[String]) => {
- val tool = dir + Path.explode(name)
- val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
- sys.exit(result.print_stdout.rc)
- }
- })
+ dirs().collectFirst(
+ {
+ case dir if is_external(dir, name + ".scala") =>
+ compile(dir + Path.explode(name + ".scala"))
+ case dir if is_external(dir, name) =>
+ { (args: List[String]) =>
+ val tool = dir + Path.explode(name)
+ val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
+ sys.exit(result.print_stdout.rc)
+ }
+ })
/* internal tools */
--- a/src/Pure/System/options.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/System/options.scala Fri Apr 01 23:19:12 2022 +0200
@@ -151,13 +151,14 @@
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options",
- Scala_Project.here, args => {
- var build_options = false
- var get_option = ""
- var list_options = false
- var export_file = ""
+ Scala_Project.here,
+ { args =>
+ var build_options = false
+ var get_option = ""
+ var list_options = false
+ var export_file = ""
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
Options are:
@@ -169,32 +170,32 @@
Report Isabelle system options, augmented by MORE_OPTIONS given as
arguments NAME=VAL or NAME.
""",
- "b" -> (_ => build_options = true),
- "g:" -> (arg => get_option = arg),
- "l" -> (_ => list_options = true),
- "x:" -> (arg => export_file = arg))
+ "b" -> (_ => build_options = true),
+ "g:" -> (arg => get_option = arg),
+ "l" -> (_ => list_options = true),
+ "x:" -> (arg => export_file = arg))
- val more_options = getopts(args)
- if (get_option == "" && !list_options && export_file == "") getopts.usage()
+ val more_options = getopts(args)
+ if (get_option == "" && !list_options && export_file == "") getopts.usage()
- val options = {
- val options0 = Options.init()
- val options1 =
- if (build_options)
- Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _)
- else options0
- more_options.foldLeft(options1)(_ + _)
- }
+ val options = {
+ val options0 = Options.init()
+ val options1 =
+ if (build_options)
+ Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _)
+ else options0
+ more_options.foldLeft(options1)(_ + _)
+ }
- if (get_option != "")
- Output.writeln(options.check_name(get_option).value, stdout = true)
+ if (get_option != "")
+ Output.writeln(options.check_name(get_option).value, stdout = true)
- if (export_file != "")
- File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
+ if (export_file != "")
+ File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
- if (get_option == "" && export_file == "")
- Output.writeln(options.print, stdout = true)
- })
+ if (get_option == "" && export_file == "")
+ Output.writeln(options.print, stdout = true)
+ })
}
--- a/src/Pure/Thy/bibtex.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Thy/bibtex.scala Fri Apr 01 23:19:12 2022 +0200
@@ -105,7 +105,7 @@
}
}
- Isabelle_System.with_tmp_dir("bibtex")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("bibtex") { tmp_dir =>
File.write(tmp_dir + Path.explode("root.bib"),
tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n"))
File.write(tmp_dir + Path.explode("root.aux"),
@@ -138,7 +138,7 @@
).partition(_._1)
}
(errors.map(_._2), warnings.map(_._2))
- })
+ }
}
object Check_Database extends Scala.Fun_String("bibtex_check_database") {
@@ -629,7 +629,7 @@
style: String = "",
chronological: Boolean = false
): String = {
- Isabelle_System.with_tmp_dir("bibtex")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("bibtex") { tmp_dir =>
/* database files */
val bib_files = bib.map(_.drop_ext)
@@ -682,6 +682,6 @@
dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse)
}
else html
- })
+ }
}
}
--- a/src/Pure/Thy/document_build.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Thy/document_build.scala Fri Apr 01 23:19:12 2022 +0200
@@ -69,7 +69,7 @@
def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = {
val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name))
db.using_statement(select)(stmt =>
- stmt.execute_query().iterator(res => {
+ stmt.execute_query().iterator({ res =>
val name = res.string(Data.name)
val sources = res.string(Data.sources)
Document_Input(name, SHA1.fake_digest(sources))
@@ -82,7 +82,7 @@
name: String
): Option[Document_Output] = {
val select = Data.table.select(sql = Data.where_equal(session_name, name))
- db.using_statement(select)(stmt => {
+ db.using_statement(select)({ stmt =>
val res = stmt.execute_query()
if (res.next()) {
val name = res.string(Data.name)
@@ -96,14 +96,14 @@
}
def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = {
- db.using_statement(Data.table.insert())(stmt => {
+ db.using_statement(Data.table.insert()){ stmt =>
stmt.string(1) = session_name
stmt.string(2) = doc.name
stmt.string(3) = doc.sources.toString
stmt.bytes(4) = doc.log_xz
stmt.bytes(5) = doc.pdf
stmt.execute()
- })
+ }
}
@@ -190,12 +190,12 @@
lazy val isabelle_logo: Option[File.Content] = {
document_logo.map(logo_name =>
- Isabelle_System.with_tmp_file("logo", ext = "pdf")(tmp_path => {
+ Isabelle_System.with_tmp_file("logo", ext = "pdf") { tmp_path =>
Logo.create_logo(logo_name, output_file = tmp_path, quiet = true)
val path = Path.basic("isabelle_logo.pdf")
val content = Bytes.read(tmp_path)
File.Content(path, content)
- }))
+ })
}
@@ -388,7 +388,7 @@
val documents =
for (doc <- context.documents)
yield {
- Isabelle_System.with_tmp_dir("document")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("document") { tmp_dir =>
progress.echo("Preparing " + context.session + "/" + doc.name + " ...")
val start = Time.now()
@@ -406,7 +406,7 @@
" (" + timing.message_hms + " elapsed time)")
document
- })
+ }
}
for (dir <- output_pdf; doc <- documents) {
@@ -421,16 +421,16 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, args => {
- var output_sources: Option[Path] = None
- var output_pdf: Option[Path] = None
- var verbose_latex = false
- var dirs: List[Path] = Nil
- var options = Options.init()
- var verbose_build = false
+ Isabelle_Tool("document", "prepare session theory document", Scala_Project.here,
+ { args =>
+ var output_sources: Option[Path] = None
+ var output_pdf: Option[Path] = None
+ var verbose_latex = false
+ var dirs: List[Path] = Nil
+ var options = Options.init()
+ var verbose_build = false
- val getopts = Getopts(
- """
+ val getopts = Getopts("""
Usage: isabelle document [OPTIONS] SESSION
Options are:
@@ -444,48 +444,48 @@
Prepare the theory document of a session.
""",
- "O:" -> (arg =>
- {
- val dir = Path.explode(arg)
- output_sources = Some(dir)
- output_pdf = Some(dir)
- }),
- "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }),
- "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }),
- "V" -> (_ => verbose_latex = true),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "o:" -> (arg => options = options + arg),
- "v" -> (_ => verbose_build = true))
+ "O:" -> (arg =>
+ {
+ val dir = Path.explode(arg)
+ output_sources = Some(dir)
+ output_pdf = Some(dir)
+ }),
+ "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }),
+ "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }),
+ "V" -> (_ => verbose_latex = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose_build = true))
- val more_args = getopts(args)
- val session =
- more_args match {
- case List(a) => a
- case _ => getopts.usage()
- }
+ val more_args = getopts(args)
+ val session =
+ more_args match {
+ case List(a) => a
+ case _ => getopts.usage()
+ }
- val progress = new Console_Progress(verbose = verbose_build)
- val store = Sessions.store(options)
+ val progress = new Console_Progress(verbose = verbose_build)
+ val store = Sessions.store(options)
- progress.interrupt_handler {
- val res =
- Build.build(options, selection = Sessions.Selection.session(session),
- dirs = dirs, progress = progress, verbose = verbose_build)
- if (!res.ok) error("Failed to build session " + quote(session))
+ progress.interrupt_handler {
+ val res =
+ Build.build(options, selection = Sessions.Selection.session(session),
+ dirs = dirs, progress = progress, verbose = verbose_build)
+ if (!res.ok) error("Failed to build session " + quote(session))
- val deps =
- Sessions.load_structure(options + "document=pdf", dirs = dirs).
- selection_deps(Sessions.Selection.session(session))
+ val deps =
+ Sessions.load_structure(options + "document=pdf", dirs = dirs).
+ selection_deps(Sessions.Selection.session(session))
- if (output_sources.isEmpty && output_pdf.isEmpty) {
- progress.echo_warning("No output directory")
- }
+ if (output_sources.isEmpty && output_pdf.isEmpty) {
+ progress.echo_warning("No output directory")
+ }
- using(store.open_database_context())(db_context => {
- build_documents(context(session, deps, db_context, progress = progress),
- output_sources = output_sources, output_pdf = output_pdf,
- verbose = verbose_latex)
- })
- }
- })
+ using(store.open_database_context()) { db_context =>
+ build_documents(context(session, deps, db_context, progress = progress),
+ output_sources = output_sources, output_pdf = output_pdf,
+ verbose = verbose_latex)
+ }
+ }
+ })
}
--- a/src/Pure/Thy/export.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Thy/export.scala Fri Apr 01 23:19:12 2022 +0200
@@ -118,7 +118,7 @@
def write(db: SQL.Database): Unit = {
val (compressed, bytes) = body.join
- db.using_statement(Data.table.insert())(stmt => {
+ db.using_statement(Data.table.insert()) { stmt =>
stmt.string(1) = session_name
stmt.string(2) = theory_name
stmt.string(3) = name
@@ -126,7 +126,7 @@
stmt.bool(5) = compressed
stmt.bytes(6) = bytes
stmt.execute()
- })
+ }
}
}
@@ -175,7 +175,7 @@
val select =
Data.table.select(List(Data.executable, Data.compressed, Data.body),
Data.where_equal(session_name, theory_name, name))
- db.using_statement(select)(stmt => {
+ db.using_statement(select) { stmt =>
val res = stmt.execute_query()
if (res.next()) {
val executable = res.bool(Data.executable)
@@ -185,7 +185,7 @@
Some(Entry(session_name, theory_name, name, executable, body, cache))
}
else None
- })
+ }
}
def read_entry(
@@ -218,7 +218,7 @@
Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
bulk = { case (entry, _) => entry.body.is_finished },
consume =
- (args: List[(Entry, Boolean)]) => {
+ { (args: List[(Entry, Boolean)]) =>
val results =
db.transaction {
for ((entry, strict) <- args)
@@ -356,7 +356,7 @@
export_list: Boolean = false,
export_patterns: List[String] = Nil
): Unit = {
- using(store.open_database(session_name))(db => {
+ using(store.open_database(session_name)) { db =>
db.transaction {
val export_names = read_theory_exports(db, session_name)
@@ -394,7 +394,7 @@
}
}
}
- })
+ }
}
@@ -402,19 +402,20 @@
val default_export_dir: Path = Path.explode("export")
- val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports",
- Scala_Project.here, args => {
- /* arguments */
+ val isabelle_tool =
+ Isabelle_Tool("export", "retrieve theory exports", Scala_Project.here,
+ { args =>
+ /* arguments */
- var export_dir = default_export_dir
- var dirs: List[Path] = Nil
- var export_list = false
- var no_build = false
- var options = Options.init()
- var export_prune = 0
- var export_patterns: List[String] = Nil
+ var export_dir = default_export_dir
+ var dirs: List[Path] = Nil
+ var export_list = false
+ var no_build = false
+ var options = Options.init()
+ var export_prune = 0
+ var export_patterns: List[String] = Nil
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle export [OPTIONS] SESSION
Options are:
@@ -433,39 +434,39 @@
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
and variants {pattern1,pattern2,pattern3}.
""",
- "O:" -> (arg => export_dir = Path.explode(arg)),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "l" -> (_ => export_list = true),
- "n" -> (_ => no_build = true),
- "o:" -> (arg => options = options + arg),
- "p:" -> (arg => export_prune = Value.Int.parse(arg)),
- "x:" -> (arg => export_patterns ::= arg))
+ "O:" -> (arg => export_dir = Path.explode(arg)),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "l" -> (_ => export_list = true),
+ "n" -> (_ => no_build = true),
+ "o:" -> (arg => options = options + arg),
+ "p:" -> (arg => export_prune = Value.Int.parse(arg)),
+ "x:" -> (arg => export_patterns ::= arg))
- val more_args = getopts(args)
- val session_name =
- more_args match {
- case List(session_name) if export_list || export_patterns.nonEmpty => session_name
- case _ => getopts.usage()
- }
+ val more_args = getopts(args)
+ val session_name =
+ more_args match {
+ case List(session_name) if export_list || export_patterns.nonEmpty => session_name
+ case _ => getopts.usage()
+ }
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- /* build */
+ /* build */
- if (!no_build) {
- val rc =
- progress.interrupt_handler {
- Build.build_logic(options, session_name, progress = progress, dirs = dirs)
+ if (!no_build) {
+ val rc =
+ progress.interrupt_handler {
+ Build.build_logic(options, session_name, progress = progress, dirs = dirs)
+ }
+ if (rc != Process_Result.RC.ok) sys.exit(rc)
}
- if (rc != Process_Result.RC.ok) sys.exit(rc)
- }
- /* export files */
+ /* export files */
- val store = Sessions.store(options)
- export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
- export_list = export_list, export_patterns = export_patterns)
- })
+ val store = Sessions.store(options)
+ export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
+ export_list = export_list, export_patterns = export_patterns)
+ })
}
--- a/src/Pure/Thy/export_theory.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala Fri Apr 01 23:19:12 2022 +0200
@@ -32,7 +32,7 @@
cache: Term.Cache = Term.Cache.make()): Session = {
val thys =
sessions_structure.build_requirements(List(session_name)).flatMap(session =>
- using(store.open_database(session))(db => {
+ using(store.open_database(session)) { db =>
db.transaction {
for (theory <- Export.read_theory_names(db, session))
yield {
@@ -41,7 +41,7 @@
read_theory(provider, session, theory, cache = cache)
}
}
- }))
+ })
val graph0 =
thys.foldLeft(Graph.string[Option[Theory]]) {
@@ -152,12 +152,12 @@
val session_name = Thy_Header.PURE
val theory_name = Thy_Header.PURE
- using(store.open_database(session_name))(db => {
+ using(store.open_database(session_name)) { db =>
db.transaction {
val provider = Export.Provider.database(db, store.cache, session_name, theory_name)
read(provider, session_name, theory_name)
}
- })
+ }
}
def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.Cache.none): Theory =
@@ -285,7 +285,7 @@
def read_types(provider: Export.Provider): List[Entity[Type]] =
read_entities(provider, Export.THEORY_PREFIX + "types", Markup.TYPE_NAME,
- body => {
+ { body =>
import XML.Decode._
val (syntax, args, abbrev) =
triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body)
@@ -313,7 +313,7 @@
def read_consts(provider: Export.Provider): List[Entity[Const]] =
read_entities(provider, Export.THEORY_PREFIX + "consts", Markup.CONSTANT,
- body => {
+ { body =>
import XML.Decode._
val (syntax, (typargs, (typ, (abbrev, propositional)))) =
pair(decode_syntax,
@@ -376,7 +376,7 @@
def read_thms(provider: Export.Provider): List[Entity[Thm]] =
read_entities(provider, Export.THEORY_PREFIX + "thms", Kind.THM,
- body => {
+ { body =>
import XML.Decode._
import Term_XML.Decode._
val (prop, deps, prf) = triple(decode_prop, list(string), proof)(body)
@@ -477,7 +477,7 @@
def read_classes(provider: Export.Provider): List[Entity[Class]] =
read_entities(provider, Export.THEORY_PREFIX + "classes", Markup.CLASS,
- body => {
+ { body =>
import XML.Decode._
import Term_XML.Decode._
val (params, axioms) = pair(list(pair(string, typ)), list(decode_prop))(body)
@@ -501,7 +501,7 @@
def read_locales(provider: Export.Provider): List[Entity[Locale]] =
read_entities(provider, Export.THEORY_PREFIX + "locales", Markup.LOCALE,
- body => {
+ { body =>
import XML.Decode._
import Term_XML.Decode._
val (typargs, args, axioms) =
@@ -534,7 +534,7 @@
def read_locale_dependencies(provider: Export.Provider): List[Entity[Locale_Dependency]] =
read_entities(provider, Export.THEORY_PREFIX + "locale_dependencies", Kind.LOCALE_DEPENDENCY,
- body => {
+ { body =>
import XML.Decode._
import Term_XML.Decode._
val (source, (target, (prefix, (subst_types, subst_terms)))) =
--- a/src/Pure/Thy/presentation.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Thy/presentation.scala Fri Apr 01 23:19:12 2022 +0200
@@ -580,7 +580,7 @@
def present_theory(name: Document.Node.Name): Option[XML.Body] = {
progress.expose_interrupt()
- Build_Job.read_theory(db_context, hierarchy, name.theory).flatMap(command => {
+ Build_Job.read_theory(db_context, hierarchy, name.theory).flatMap { command =>
if (verbose) progress.echo("Presenting theory " + name)
val snapshot = Document.State.init.snippet(command)
@@ -641,7 +641,7 @@
(if (files.isEmpty) Nil else List(HTML.itemize(files))))))
}
else None
- })
+ }
}
val theories = base.session_theories.flatMap(present_theory)
--- a/src/Pure/Thy/sessions.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Apr 01 23:19:12 2022 +0200
@@ -1057,17 +1057,18 @@
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions",
- Scala_Project.here, args => {
- var base_sessions: List[String] = Nil
- var select_dirs: List[Path] = Nil
- var requirements = false
- var exclude_session_groups: List[String] = Nil
- var all_sessions = false
- var dirs: List[Path] = Nil
- var session_groups: List[String] = Nil
- var exclude_sessions: List[String] = Nil
+ Scala_Project.here,
+ { args =>
+ var base_sessions: List[String] = Nil
+ var select_dirs: List[Path] = Nil
+ var requirements = false
+ var exclude_session_groups: List[String] = Nil
+ var all_sessions = false
+ var dirs: List[Path] = Nil
+ var session_groups: List[String] = Nil
+ var exclude_sessions: List[String] = Nil
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle sessions [OPTIONS] [SESSIONS ...]
Options are:
@@ -1083,30 +1084,30 @@
Explore the structure of Isabelle sessions and print result names in
topological order (on stdout).
""",
- "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
- "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
- "R" -> (_ => requirements = true),
- "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
- "a" -> (_ => all_sessions = true),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "g:" -> (arg => session_groups = session_groups ::: List(arg)),
- "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+ "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
+ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "R" -> (_ => requirements = true),
+ "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+ "a" -> (_ => all_sessions = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
- val sessions = getopts(args)
+ val sessions = getopts(args)
- val options = Options.init()
+ val options = Options.init()
- val selection =
- Selection(requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions,
- exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions,
- session_groups = session_groups, sessions = sessions)
- val sessions_structure =
- load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
+ val selection =
+ Selection(requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions,
+ exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions,
+ session_groups = session_groups, sessions = sessions)
+ val sessions_structure =
+ load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
- for (name <- sessions_structure.imports_topological_order) {
- Output.writeln(name, stdout = true)
- }
- })
+ for (name <- sessions_structure.imports_topological_order) {
+ Output.writeln(name, stdout = true)
+ }
+ })
@@ -1116,7 +1117,7 @@
def read_heap_digest(heap: Path): Option[String] = {
if (heap.is_file) {
- using(FileChannel.open(heap.java_path, StandardOpenOption.READ))(file => {
+ using(FileChannel.open(heap.java_path, StandardOpenOption.READ)) { file =>
val len = file.size
val n = sha1_prefix.length + SHA1.digest_length
if (len >= n) {
@@ -1140,7 +1141,7 @@
else None
}
else None
- })
+ }
}
else None
}
@@ -1374,10 +1375,10 @@
def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
db.using_statement(Session_Info.table.select(List(column),
- Session_Info.session_name.where_equal(name)))(stmt => {
+ Session_Info.session_name.where_equal(name))) { stmt =>
val res = stmt.execute_query()
if (!res.next()) Bytes.empty else res.bytes(column)
- })
+ }
def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
Properties.uncompress(read_bytes(db, name, column), cache = cache)
@@ -1424,7 +1425,7 @@
build: Build.Session_Info
): Unit = {
db.transaction {
- db.using_statement(Session_Info.table.insert())(stmt => {
+ db.using_statement(Session_Info.table.insert()) { stmt =>
stmt.string(1) = name
stmt.bytes(2) = Properties.encode(build_log.session_timing)
stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.xz)
@@ -1437,7 +1438,7 @@
stmt.string(10) = build.output_heap getOrElse ""
stmt.int(11) = build.return_code
stmt.execute()
- })
+ }
}
}
@@ -1465,7 +1466,7 @@
def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = {
if (db.tables.contains(Session_Info.table.name)) {
db.using_statement(Session_Info.table.select(Session_Info.build_columns,
- Session_Info.session_name.where_equal(name)))(stmt => {
+ Session_Info.session_name.where_equal(name))) { stmt =>
val res = stmt.execute_query()
if (!res.next()) None
else {
@@ -1476,7 +1477,7 @@
res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
res.int(Session_Info.return_code)))
}
- })
+ }
}
else None
}
--- a/src/Pure/Tools/build.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/build.scala Fri Apr 01 23:19:12 2022 +0200
@@ -70,11 +70,11 @@
else {
val descendants = sessions_structure.build_descendants(List(session_name)).toSet
val g = sessions_structure.build_graph.restrict(descendants)
- (0.0 :: g.maximals.flatMap(desc => {
+ (0.0 :: g.maximals.flatMap { desc =>
val ps = g.all_preds(List(desc))
if (ps.exists(p => !timing.isDefinedAt(p))) None
else Some(ps.map(timing(_)).sum)
- })).max
+ }).max
}
}
timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
@@ -494,11 +494,11 @@
Presentation.update_chapter(presentation_dir, chapter, entries)
}
- using(store.open_database_context())(db_context => {
+ using(store.open_database_context()) { db_context =>
val exports =
Presentation.read_exports(presentation_sessions.map(_.name), deps, db_context)
- Par_List.map((session: String) => {
+ Par_List.map({ (session: String) =>
progress.expose_interrupt()
progress.echo("Presenting " + session + " ...")
@@ -514,7 +514,7 @@
verbose = verbose, html_context = html_context,
Presentation.elements1)
}, presentation_sessions.map(_.name))
- })
+ }
}
}
@@ -525,32 +525,33 @@
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions",
- Scala_Project.here, args => {
- val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
+ Scala_Project.here,
+ { args =>
+ val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
- var base_sessions: List[String] = Nil
- var select_dirs: List[Path] = Nil
- var numa_shuffling = false
- var presentation = Presentation.Context.none
- var requirements = false
- var soft_build = false
- var exclude_session_groups: List[String] = Nil
- var all_sessions = false
- var build_heap = false
- var clean_build = false
- var dirs: List[Path] = Nil
- var export_files = false
- var fresh_build = false
- var session_groups: List[String] = Nil
- var max_jobs = 1
- var check_keywords: Set[String] = Set.empty
- var list_files = false
- var no_build = false
- var options = Options.init(opts = build_options)
- var verbose = false
- var exclude_sessions: List[String] = Nil
+ var base_sessions: List[String] = Nil
+ var select_dirs: List[Path] = Nil
+ var numa_shuffling = false
+ var presentation = Presentation.Context.none
+ var requirements = false
+ var soft_build = false
+ var exclude_session_groups: List[String] = Nil
+ var all_sessions = false
+ var build_heap = false
+ var clean_build = false
+ var dirs: List[Path] = Nil
+ var export_files = false
+ var fresh_build = false
+ var session_groups: List[String] = Nil
+ var max_jobs = 1
+ var check_keywords: Set[String] = Set.empty
+ var list_files = false
+ var no_build = false
+ var options = Options.init(opts = build_options)
+ var verbose = false
+ var exclude_sessions: List[String] = Nil
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
@@ -579,83 +580,83 @@
Build and manage Isabelle sessions, depending on implicit settings:
""" + Library.indent_lines(2, Build_Log.Settings.show()) + "\n",
- "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
- "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
- "N" -> (_ => numa_shuffling = true),
- "P:" -> (arg => presentation = Presentation.Context.make(arg)),
- "R" -> (_ => requirements = true),
- "S" -> (_ => soft_build = true),
- "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
- "a" -> (_ => all_sessions = true),
- "b" -> (_ => build_heap = true),
- "c" -> (_ => clean_build = true),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "e" -> (_ => export_files = true),
- "f" -> (_ => fresh_build = true),
- "g:" -> (arg => session_groups = session_groups ::: List(arg)),
- "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
- "k:" -> (arg => check_keywords = check_keywords + arg),
- "l" -> (_ => list_files = true),
- "n" -> (_ => no_build = true),
- "o:" -> (arg => options = options + arg),
- "v" -> (_ => verbose = true),
- "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+ "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
+ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "N" -> (_ => numa_shuffling = true),
+ "P:" -> (arg => presentation = Presentation.Context.make(arg)),
+ "R" -> (_ => requirements = true),
+ "S" -> (_ => soft_build = true),
+ "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+ "a" -> (_ => all_sessions = true),
+ "b" -> (_ => build_heap = true),
+ "c" -> (_ => clean_build = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "e" -> (_ => export_files = true),
+ "f" -> (_ => fresh_build = true),
+ "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+ "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+ "k:" -> (arg => check_keywords = check_keywords + arg),
+ "l" -> (_ => list_files = true),
+ "n" -> (_ => no_build = true),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose = true),
+ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
- val sessions = getopts(args)
+ val sessions = getopts(args)
- val progress = new Console_Progress(verbose = verbose)
+ val progress = new Console_Progress(verbose = verbose)
- val start_date = Date.now()
+ val start_date = Date.now()
- if (verbose) {
- progress.echo(
- "Started at " + Build_Log.print_date(start_date) +
- " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
- progress.echo(Build_Log.Settings.show() + "\n")
- }
+ if (verbose) {
+ progress.echo(
+ "Started at " + Build_Log.print_date(start_date) +
+ " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
+ progress.echo(Build_Log.Settings.show() + "\n")
+ }
- val results =
- progress.interrupt_handler {
- build(options,
- selection = Sessions.Selection(
- requirements = requirements,
- all_sessions = all_sessions,
- base_sessions = base_sessions,
- exclude_session_groups = exclude_session_groups,
- exclude_sessions = exclude_sessions,
- session_groups = session_groups,
- sessions = sessions),
- presentation = presentation,
- progress = progress,
- check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
- build_heap = build_heap,
- clean_build = clean_build,
- dirs = dirs,
- select_dirs = select_dirs,
- numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
- max_jobs = max_jobs,
- list_files = list_files,
- check_keywords = check_keywords,
- fresh_build = fresh_build,
- no_build = no_build,
- soft_build = soft_build,
- verbose = verbose,
- export_files = export_files)
+ val results =
+ progress.interrupt_handler {
+ build(options,
+ selection = Sessions.Selection(
+ requirements = requirements,
+ all_sessions = all_sessions,
+ base_sessions = base_sessions,
+ exclude_session_groups = exclude_session_groups,
+ exclude_sessions = exclude_sessions,
+ session_groups = session_groups,
+ sessions = sessions),
+ presentation = presentation,
+ progress = progress,
+ check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
+ build_heap = build_heap,
+ clean_build = clean_build,
+ dirs = dirs,
+ select_dirs = select_dirs,
+ numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
+ max_jobs = max_jobs,
+ list_files = list_files,
+ check_keywords = check_keywords,
+ fresh_build = fresh_build,
+ no_build = no_build,
+ soft_build = soft_build,
+ verbose = verbose,
+ export_files = export_files)
+ }
+ val end_date = Date.now()
+ val elapsed_time = end_date.time - start_date.time
+
+ if (verbose) {
+ progress.echo("\nFinished at " + Build_Log.print_date(end_date))
}
- val end_date = Date.now()
- val elapsed_time = end_date.time - start_date.time
-
- if (verbose) {
- progress.echo("\nFinished at " + Build_Log.print_date(end_date))
- }
- val total_timing =
- results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
- copy(elapsed = elapsed_time)
- progress.echo(total_timing.message_resources)
+ val total_timing =
+ results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
+ copy(elapsed = elapsed_time)
+ progress.echo(total_timing.message_resources)
- sys.exit(results.rc)
- })
+ sys.exit(results.rc)
+ })
/* build logic image */
--- a/src/Pure/Tools/build_docker.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/build_docker.scala Fri Apr 01 23:19:12 2022 +0200
@@ -77,21 +77,21 @@
output.foreach(File.write(_, dockerfile))
if (!no_build) {
- Isabelle_System.with_tmp_dir("docker")(tmp_dir => {
- File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
+ Isabelle_System.with_tmp_dir("docker") { tmp_dir =>
+ File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
- if (is_remote) {
- if (!Url.is_readable(app_archive))
- error("Cannot access remote archive " + app_archive)
- }
- else Isabelle_System.copy_file(Path.explode(app_archive),
- tmp_dir + Path.explode("Isabelle.tar.gz"))
+ if (is_remote) {
+ if (!Url.is_readable(app_archive))
+ error("Cannot access remote archive " + app_archive)
+ }
+ else Isabelle_System.copy_file(Path.explode(app_archive),
+ tmp_dir + Path.explode("Isabelle.tar.gz"))
- val quiet_option = if (verbose) "" else " -q"
- val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
- progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
- echo = true).check
- })
+ val quiet_option = if (verbose) "" else " -q"
+ val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
+ progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
+ echo = true).check
+ }
}
}
@@ -100,18 +100,18 @@
val isabelle_tool =
Isabelle_Tool("build_docker", "build Isabelle docker image",
- Scala_Project.here, args => {
- var base = default_base
- var entrypoint = false
- var logic = default_logic
- var no_build = false
- var output: Option[Path] = None
- var more_packages: List[String] = Nil
- var verbose = false
- var tag = ""
+ Scala_Project.here,
+ { args =>
+ var base = default_base
+ var entrypoint = false
+ var logic = default_logic
+ var no_build = false
+ var output: Option[Path] = None
+ var more_packages: List[String] = Nil
+ var verbose = false
+ var tag = ""
- val getopts =
- Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
Options are:
@@ -143,15 +143,15 @@
"t:" -> (arg => tag = arg),
"v" -> (_ => verbose = true))
- val more_args = getopts(args)
- val app_archive =
- more_args match {
- case List(arg) => arg
- case _ => getopts.usage()
- }
+ val more_args = getopts(args)
+ val app_archive =
+ more_args match {
+ case List(arg) => arg
+ case _ => getopts.usage()
+ }
- build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
- no_build = no_build, entrypoint = entrypoint, output = output,
- more_packages = more_packages, tag = tag, verbose = verbose)
- })
+ build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
+ no_build = no_build, entrypoint = entrypoint, output = output,
+ more_packages = more_packages, tag = tag, verbose = verbose)
+ })
}
--- a/src/Pure/Tools/build_job.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/build_job.scala Fri Apr 01 23:19:12 2022 +0200
@@ -39,12 +39,12 @@
yield i -> elem)
val blobs =
- blobs_files.map(file => {
+ blobs_files.map { file =>
val path = Path.explode(file)
val name = Resources.file_node(path)
val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
Command.Blob(name, src_path, None)
- })
+ }
val blobs_xml =
for (i <- (1 to blobs.length).toList)
yield read_xml(Export.MARKUP + i)
@@ -94,13 +94,13 @@
val store = Sessions.store(options)
val session = new Session(options, Resources.empty)
- using(store.open_database_context())(db_context => {
+ using(store.open_database_context()) { db_context =>
val result =
- db_context.input_database(session_name)((db, _) => {
+ db_context.input_database(session_name) { (db, _) =>
val theories = store.read_theories(db, session_name)
val errors = store.read_errors(db, session_name)
store.read_build(db, session_name).map(info => (theories, errors, info.return_code))
- })
+ }
result match {
case None => error("Missing build database for session " + quote(session_name))
case Some((used_theories, errors, rc)) =>
@@ -143,23 +143,24 @@
progress.echo("\n" + Process_Result.RC.print_long(rc))
}
}
- })
+ }
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("log", "print messages from build database",
- Scala_Project.here, args => {
- /* arguments */
+ Scala_Project.here,
+ { args =>
+ /* arguments */
- var unicode_symbols = false
- var theories: List[String] = Nil
- var margin = Pretty.default_margin
- var options = Options.init()
- var verbose = false
+ var unicode_symbols = false
+ var theories: List[String] = Nil
+ var margin = Pretty.default_margin
+ var options = Options.init()
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle log [OPTIONS] SESSION
Options are:
@@ -173,24 +174,24 @@
checks against current sources: results from a failed build can be
printed as well.
""",
- "T:" -> (arg => theories = theories ::: List(arg)),
- "U" -> (_ => unicode_symbols = true),
- "m:" -> (arg => margin = Value.Double.parse(arg)),
- "o:" -> (arg => options = options + arg),
- "v" -> (_ => verbose = true))
+ "T:" -> (arg => theories = theories ::: List(arg)),
+ "U" -> (_ => unicode_symbols = true),
+ "m:" -> (arg => margin = Value.Double.parse(arg)),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- val session_name =
- more_args match {
- case List(session_name) => session_name
- case _ => getopts.usage()
- }
+ val more_args = getopts(args)
+ val session_name =
+ more_args match {
+ case List(session_name) => session_name
+ case _ => getopts.usage()
+ }
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- print_log(options, session_name, theories = theories, verbose = verbose, margin = margin,
- progress = progress, unicode_symbols = unicode_symbols)
- })
+ print_log(options, session_name, theories = theories, verbose = verbose, margin = margin,
+ progress = progress, unicode_symbols = unicode_symbols)
+ })
}
class Build_Job(progress: Progress,
@@ -442,16 +443,16 @@
val (document_output, document_errors) =
try {
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
- using(store.open_database_context())(db_context => {
- val documents =
- Document_Build.build_documents(
- Document_Build.context(session_name, deps, db_context, progress = progress),
- output_sources = info.document_output,
- output_pdf = info.document_output)
- db_context.output_database(session_name)(db =>
- documents.foreach(_.write(db, session_name)))
- (documents.flatMap(_.log_lines), Nil)
- })
+ using(store.open_database_context()) { db_context =>
+ val documents =
+ Document_Build.build_documents(
+ Document_Build.context(session_name, deps, db_context, progress = progress),
+ output_sources = info.document_output,
+ output_pdf = info.document_output)
+ db_context.output_database(session_name)(db =>
+ documents.foreach(_.write(db, session_name)))
+ (documents.flatMap(_.log_lines), Nil)
+ }
}
else (Nil, Nil)
}
--- a/src/Pure/Tools/check_keywords.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/check_keywords.scala Fri Apr 01 23:19:12 2022 +0200
@@ -38,7 +38,7 @@
val parallel_args = paths.map(path => (File.read(path), Token.Pos.file(path.expand.implode)))
val bad =
- Par_List.map((arg: (String, Token.Pos)) => {
+ Par_List.map({ (arg: (String, Token.Pos)) =>
progress.expose_interrupt()
conflicts(keywords, check, arg._1, arg._2)
}, parallel_args).flatten
--- a/src/Pure/Tools/debugger.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/debugger.scala Fri Apr 01 23:19:12 2022 +0200
@@ -171,28 +171,28 @@
}
def init(): Unit =
- state.change(st => {
+ state.change { st =>
val st1 = st.inc_active
if (session.is_ready && !st.is_active && st1.is_active)
session.protocol_command("Debugger.init")
st1
- })
+ }
def exit(): Unit =
- state.change(st => {
+ state.change { st =>
val st1 = st.dec_active
if (session.is_ready && st.is_active && !st1.is_active)
session.protocol_command("Debugger.exit")
st1
- })
+ }
def is_break(): Boolean = state.value.break
def set_break(b: Boolean): Unit = {
- state.change(st => {
+ state.change { st =>
val st1 = st.set_break(b)
session.protocol_command("Debugger.break", b.toString)
st1
- })
+ }
delay_update.invoke()
}
@@ -205,7 +205,7 @@
state.value.active_breakpoints(breakpoint)
def toggle_breakpoint(command: Command, breakpoint: Long): Unit = {
- state.change(st => {
+ state.change { st =>
val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint)
session.protocol_command(
"Debugger.breakpoint",
@@ -214,7 +214,7 @@
Value.Long(breakpoint),
Value.Boolean(breakpoint_state))
st1
- })
+ }
}
def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) = {
@@ -252,22 +252,22 @@
}
def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String): Unit = {
- state.change(st => {
+ state.change { st =>
input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString,
SML.toString, Symbol.encode(context), Symbol.encode(expression))
st.clear_output(c.thread_name)
- })
+ }
delay_update.invoke()
}
def print_vals(c: Debugger.Context, SML: Boolean, context: String): Unit = {
require(c.debug_index.isDefined)
- state.change(st => {
+ state.change { st =>
input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString,
SML.toString, Symbol.encode(context))
st.clear_output(c.thread_name)
- })
+ }
delay_update.invoke()
}
}
--- a/src/Pure/Tools/doc.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/doc.scala Fri Apr 01 23:19:12 2022 +0200
@@ -128,22 +128,23 @@
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("doc", "view Isabelle PDF documentation",
- Scala_Project.here, args => {
- val getopts = Getopts("""
+ Scala_Project.here,
+ { args =>
+ val getopts = Getopts("""
Usage: isabelle doc [DOC ...]
View Isabelle PDF documentation.
""")
- val docs = getopts(args)
+ val docs = getopts(args)
- if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
- else {
- docs.foreach(name =>
- contents().docs.find(_.name == name) match {
- case Some(doc) => view(doc.path)
- case None => error("No Isabelle documentation entry: " + quote(name))
- }
- )
- }
- })
+ if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
+ else {
+ docs.foreach(name =>
+ contents().docs.find(_.name == name) match {
+ case Some(doc) => view(doc.path)
+ case None => error("No Isabelle documentation entry: " + quote(name))
+ }
+ )
+ }
+ })
}
--- a/src/Pure/Tools/dump.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/dump.scala Fri Apr 01 23:19:12 2022 +0200
@@ -298,37 +298,37 @@
private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory])
private val consumer =
- Consumer_Thread.fork(name = "dump")(
- consume = (args: (Document.Snapshot, Document_Status.Node_Status)) => {
- val (snapshot, status) = args
- val name = snapshot.node_name
- if (status.ok) {
- try {
- if (context.process_theory(name.theory)) {
- process_theory(Args(session, snapshot, status))
- }
- }
- catch {
- case exn: Throwable if !Exn.is_interrupt(exn) =>
- val msg = Exn.message(exn)
- progress.echo("FAILED to process theory " + name)
- progress.echo_error_message(msg)
- consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
+ Consumer_Thread.fork(name = "dump")(consume =
+ { (args: (Document.Snapshot, Document_Status.Node_Status)) =>
+ val (snapshot, status) = args
+ val name = snapshot.node_name
+ if (status.ok) {
+ try {
+ if (context.process_theory(name.theory)) {
+ process_theory(Args(session, snapshot, status))
}
}
- else {
- val msgs =
- for ((elem, pos) <- snapshot.messages if Protocol.is_error(elem))
- yield {
- "Error" + Position.here(pos) + ":\n" +
- XML.content(Pretty.formatted(List(elem)))
- }
- progress.echo("FAILED to process theory " + name)
- msgs.foreach(progress.echo_error_message)
- consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
+ catch {
+ case exn: Throwable if !Exn.is_interrupt(exn) =>
+ val msg = Exn.message(exn)
+ progress.echo("FAILED to process theory " + name)
+ progress.echo_error_message(msg)
+ consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
}
- true
- })
+ }
+ else {
+ val msgs =
+ for ((elem, pos) <- snapshot.messages if Protocol.is_error(elem))
+ yield {
+ "Error" + Position.here(pos) + ":\n" +
+ XML.content(Pretty.formatted(List(elem)))
+ }
+ progress.echo("FAILED to process theory " + name)
+ msgs.foreach(progress.echo_error_message)
+ consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
+ }
+ true
+ })
def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit =
consumer.send((snapshot, status))
@@ -393,13 +393,13 @@
context.build_logic(logic)
for (session <- context.sessions(logic = logic, log = log)) {
- session.process((args: Args) => {
- progress.echo("Processing theory " + args.print_node + " ...")
- val aspect_args =
- Aspect_Args(session.options, context.deps, progress, output_dir,
- args.snapshot, args.status)
- aspects.foreach(_.operation(aspect_args))
- })
+ session.process({ (args: Args) =>
+ progress.echo("Processing theory " + args.print_node + " ...")
+ val aspect_args =
+ Aspect_Args(session.options, context.deps, progress, output_dir,
+ args.snapshot, args.status)
+ aspects.foreach(_.operation(aspect_args))
+ })
}
context.check_errors
@@ -410,22 +410,22 @@
val isabelle_tool =
Isabelle_Tool("dump", "dump cumulative PIDE session database", Scala_Project.here,
- args => {
- var aspects: List[Aspect] = known_aspects
- var base_sessions: List[String] = Nil
- var select_dirs: List[Path] = Nil
- var output_dir = default_output_dir
- var requirements = false
- var exclude_session_groups: List[String] = Nil
- var all_sessions = false
- var logic = default_logic
- var dirs: List[Path] = Nil
- var session_groups: List[String] = Nil
- var options = Options.init()
- var verbose = false
- var exclude_sessions: List[String] = Nil
+ { args =>
+ var aspects: List[Aspect] = known_aspects
+ var base_sessions: List[String] = Nil
+ var select_dirs: List[Path] = Nil
+ var output_dir = default_output_dir
+ var requirements = false
+ var exclude_session_groups: List[String] = Nil
+ var all_sessions = false
+ var logic = default_logic
+ var dirs: List[Path] = Nil
+ var session_groups: List[String] = Nil
+ var options = Options.init()
+ var verbose = false
+ var exclude_sessions: List[String] = Nil
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle dump [OPTIONS] [SESSIONS ...]
Options are:
@@ -446,49 +446,49 @@
Dump cumulative PIDE session database, with the following aspects:
""" + Library.indent_lines(4, show_aspects) + "\n",
- "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect)),
- "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
- "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
- "O:" -> (arg => output_dir = Path.explode(arg)),
- "R" -> (_ => requirements = true),
- "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
- "a" -> (_ => all_sessions = true),
- "b:" -> (arg => logic = arg),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "g:" -> (arg => session_groups = session_groups ::: List(arg)),
- "o:" -> (arg => options = options + arg),
- "v" -> (_ => verbose = true),
- "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+ "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect)),
+ "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
+ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "O:" -> (arg => output_dir = Path.explode(arg)),
+ "R" -> (_ => requirements = true),
+ "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+ "a" -> (_ => all_sessions = true),
+ "b:" -> (arg => logic = arg),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose = true),
+ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
- val sessions = getopts(args)
+ val sessions = getopts(args)
- val progress = new Console_Progress(verbose = verbose)
+ val progress = new Console_Progress(verbose = verbose)
- val start_date = Date.now()
+ val start_date = Date.now()
- progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date))
+ progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date))
- progress.interrupt_handler {
- dump(options, logic,
- aspects = aspects,
- progress = progress,
- dirs = dirs,
- select_dirs = select_dirs,
- output_dir = output_dir,
- selection = Sessions.Selection(
- requirements = requirements,
- all_sessions = all_sessions,
- base_sessions = base_sessions,
- exclude_session_groups = exclude_session_groups,
- exclude_sessions = exclude_sessions,
- session_groups = session_groups,
- sessions = sessions))
- }
+ progress.interrupt_handler {
+ dump(options, logic,
+ aspects = aspects,
+ progress = progress,
+ dirs = dirs,
+ select_dirs = select_dirs,
+ output_dir = output_dir,
+ selection = Sessions.Selection(
+ requirements = requirements,
+ all_sessions = all_sessions,
+ base_sessions = base_sessions,
+ exclude_session_groups = exclude_session_groups,
+ exclude_sessions = exclude_sessions,
+ session_groups = session_groups,
+ sessions = sessions))
+ }
- val end_date = Date.now()
- val timing = end_date.time - start_date.time
+ val end_date = Date.now()
+ val timing = end_date.time - start_date.time
- progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date))
- progress.echo(timing.message_hms + " elapsed time")
- })
+ progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date))
+ progress.echo(timing.message_hms + " elapsed time")
+ })
}
--- a/src/Pure/Tools/fontforge.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/fontforge.scala Fri Apr 01 23:19:12 2022 +0200
@@ -67,11 +67,11 @@
/** execute fontforge program **/
def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result =
- Isabelle_System.with_tmp_file("fontforge")(script_file => {
+ Isabelle_System.with_tmp_file("fontforge") { script_file =>
File.write(script_file, script)
Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) +
" -lang=ff -script " + File.bash_path(script_file) + " " + args)
- })
+ }
def font_domain(path: Path, strict: Boolean = false): List[Int] = {
val script =
--- a/src/Pure/Tools/logo.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/logo.scala Fri Apr 01 23:19:12 2022 +0200
@@ -16,7 +16,7 @@
}
def create_logo(logo_name: String, output_file: Path, quiet: Boolean = false): Unit = {
- Isabelle_System.with_tmp_file("logo", ext = "eps")(tmp_file => {
+ Isabelle_System.with_tmp_file("logo", ext = "eps") { tmp_file =>
val template = File.read(Path.explode("$ISABELLE_HOME/lib/logo/isabelle_any.eps"))
File.write(tmp_file, template.replace("<any>", logo_name))
@@ -24,7 +24,7 @@
"\"$ISABELLE_EPSTOPDF\" --filter < " + File.bash_path(tmp_file) +
" > " + File.bash_path(output_file)).check
if (!quiet) Output.writeln(output_file.expand.implode)
- })
+ }
}
@@ -32,11 +32,11 @@
val isabelle_tool =
Isabelle_Tool("logo", "create variants of the Isabelle logo (PDF)", Scala_Project.here,
- args => {
- var output: Option[Path] = None
- var quiet = false
+ { args =>
+ var output: Option[Path] = None
+ var quiet = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle logo [OPTIONS] [NAME]
Options are:
@@ -45,16 +45,16 @@
Create variant NAME of the Isabelle logo as "isabelle_name.pdf".
""",
- "o:" -> (arg => output = Some(Path.explode(arg))),
- "q" -> (_ => quiet = true))
+ "o:" -> (arg => output = Some(Path.explode(arg))),
+ "q" -> (_ => quiet = true))
- val more_args = getopts(args)
- val logo_name =
- more_args match {
- case Nil => ""
- case List(name) => name
- case _ => getopts.usage()
- }
- create_logo(logo_name, output getOrElse make_output_file(logo_name), quiet = quiet)
- })
+ val more_args = getopts(args)
+ val logo_name =
+ more_args match {
+ case Nil => ""
+ case List(name) => name
+ case _ => getopts.usage()
+ }
+ create_logo(logo_name, output getOrElse make_output_file(logo_name), quiet = quiet)
+ })
}
--- a/src/Pure/Tools/mkroot.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/mkroot.scala Fri Apr 01 23:19:12 2022 +0200
@@ -178,13 +178,13 @@
val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory",
Scala_Project.here,
- args => {
- var author = ""
- var init_repos = false
- var title = ""
- var session_name = ""
+ { args =>
+ var author = ""
+ var init_repos = false
+ var title = ""
+ var session_name = ""
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
Options are:
@@ -195,21 +195,21 @@
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))
+ "A:" -> (arg => author = arg),
+ "I" -> (arg => init_repos = true),
+ "T:" -> (arg => title = arg),
+ "n:" -> (arg => session_name = arg))
- val more_args = getopts(args)
+ val more_args = getopts(args)
- val session_dir =
- more_args match {
- case Nil => Path.current
- case List(dir) => Path.explode(dir)
- case _ => getopts.usage()
- }
+ val session_dir =
+ more_args match {
+ case Nil => Path.current
+ case List(dir) => Path.explode(dir)
+ case _ => getopts.usage()
+ }
- mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
- 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)
+ })
}
--- a/src/Pure/Tools/phabricator.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/phabricator.scala Fri Apr 01 23:19:12 2022 +0200
@@ -133,12 +133,11 @@
val isabelle_tool1 =
Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory",
Scala_Project.here,
- args => {
- var list = false
- var name = default_name
+ { args =>
+ var list = false
+ var name = default_name
- val getopts =
- Getopts("""
+ val getopts = Getopts("""
Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]
Options are:
@@ -151,22 +150,22 @@
"l" -> (_ => list = true),
"n:" -> (arg => name = arg))
- val more_args = getopts(args)
- if (more_args.isEmpty && !list) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.isEmpty && !list) getopts.usage()
- val progress = new Console_Progress
+ val progress = new Console_Progress
- if (list) {
- for (config <- read_config()) {
- progress.echo("phabricator " + quote(config.name) + " root " + config.root)
+ if (list) {
+ for (config <- read_config()) {
+ progress.echo("phabricator " + quote(config.name) + " root " + config.root)
+ }
}
- }
- else {
- val config = get_config(name)
- val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true)
- if (!result.ok) error(result.print_return_code)
- }
- })
+ else {
+ val config = get_config(name)
+ val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true)
+ if (!result.ok) error(result.print_return_code)
+ }
+ })
@@ -196,7 +195,7 @@
def mercurial_setup(mercurial_source: String, progress: Progress = new Progress): Unit = {
progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...")
- Isabelle_System.with_tmp_dir("mercurial")(tmp_dir => {
+ Isabelle_System.with_tmp_dir("mercurial") { tmp_dir =>
val archive =
if (Url.is_wellformed(mercurial_source)) {
val archive = tmp_dir + Path.basic("mercurial.tar.gz")
@@ -209,7 +208,7 @@
val build_dir = tmp_dir + Path.basic(File.get_dir(tmp_dir))
progress.bash("make all && make install", cwd = build_dir.file, echo = true).check
- })
+ }
}
def phabricator_setup(
@@ -519,16 +518,15 @@
val isabelle_tool2 =
Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux",
Scala_Project.here,
- args => {
- var mercurial_source = ""
- var repo = ""
- var package_update = false
- var name = default_name
- var options = Options.init()
- var root = ""
+ { args =>
+ var mercurial_source = ""
+ var repo = ""
+ var package_update = false
+ var name = default_name
+ var options = Options.init()
+ var root = ""
- val getopts =
- Getopts("""
+ val getopts = Getopts("""
Usage: isabelle phabricator_setup [OPTIONS]
Options are:
@@ -552,14 +550,14 @@
"o:" -> (arg => options = options + arg),
"r:" -> (arg => root = arg))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress
+ val progress = new Console_Progress
- phabricator_setup(options, name = name, root = root, repo = repo,
- package_update = package_update, mercurial_source = mercurial_source, progress = progress)
- })
+ phabricator_setup(options, name = name, root = root, repo = repo,
+ package_update = package_update, mercurial_source = mercurial_source, progress = progress)
+ })
@@ -626,13 +624,12 @@
val isabelle_tool3 =
Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phabricator installation",
Scala_Project.here,
- args => {
- var test_user = ""
- var name = default_name
- var config_file: Option[Path] = None
+ { args =>
+ var test_user = ""
+ var name = default_name
+ var config_file: Option[Path] = None
- val getopts =
- Getopts("""
+ val getopts = Getopts("""
Usage: isabelle phabricator_setup_mail [OPTIONS]
Options are:
@@ -646,14 +643,14 @@
"f:" -> (arg => config_file = Some(Path.explode(arg))),
"n:" -> (arg => name = arg))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress
+ val progress = new Console_Progress
- phabricator_setup_mail(name = name, config_file = config_file,
- test_user = test_user, progress = progress)
- })
+ phabricator_setup_mail(name = name, config_file = config_file,
+ test_user = test_user, progress = progress)
+ })
@@ -787,12 +784,11 @@
val isabelle_tool4 =
Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phabricator installations",
Scala_Project.here,
- args => {
- var server_port = default_server_port
- var system_port = default_system_port
+ { args =>
+ var server_port = default_server_port
+ var system_port = default_system_port
- val getopts =
- Getopts("""
+ val getopts = Getopts("""
Usage: isabelle phabricator_setup_ssh [OPTIONS]
Options are:
@@ -810,14 +806,14 @@
"p:" -> (arg => server_port = Value.Int.parse(arg)),
"q:" -> (arg => system_port = Value.Int.parse(arg)))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress
+ val progress = new Console_Progress
- phabricator_setup_ssh(
- server_port = server_port, system_port = system_port, progress = progress)
- })
+ phabricator_setup_ssh(
+ server_port = server_port, system_port = system_port, progress = progress)
+ })
@@ -912,14 +908,14 @@
/* execute methods */
def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T = {
- Isabelle_System.with_tmp_file("params", "json")(params_file => {
+ Isabelle_System.with_tmp_file("params", "json") { params_file =>
File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params))))
val result =
Isabelle_System.bash(
"ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) +
" conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check
JSON.parse(result.out, strict = false)
- })
+ }
}
def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result =
--- a/src/Pure/Tools/profiling_report.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/profiling_report.scala Fri Apr 01 23:19:12 2022 +0200
@@ -17,7 +17,7 @@
): Unit = {
val store = Sessions.store(options)
- using(store.open_database_context())(db_context => {
+ using(store.open_database_context()) { db_context =>
val result =
db_context.input_database(session)((db, name) => Some(store.read_theories(db, name)))
result match {
@@ -38,7 +38,7 @@
for (report <- ML_Profiling.account(reports)) progress.echo(report.print)
}
- })
+ }
}
@@ -47,13 +47,12 @@
val isabelle_tool =
Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files",
Scala_Project.here,
- args => {
- var theories: List[String] = Nil
- var clean_name = false
- var options = Options.init()
+ { args =>
+ var theories: List[String] = Nil
+ var clean_name = false
+ var options = Options.init()
- val getopts =
- Getopts("""
+ val getopts = Getopts("""
Usage: isabelle profiling_report [OPTIONS] SESSION
Options are:
@@ -68,16 +67,16 @@
"c" -> (_ => clean_name = true),
"o:" -> (arg => options = options + arg))
- val more_args = getopts(args)
- val session_name =
- more_args match {
- case List(session_name) => session_name
- case _ => getopts.usage()
- }
+ val more_args = getopts(args)
+ val session_name =
+ more_args match {
+ case List(session_name) => session_name
+ case _ => getopts.usage()
+ }
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- profiling_report(options, session_name, theories = theories,
- clean_name = clean_name, progress = progress)
- })
+ profiling_report(options, session_name, theories = theories,
+ clean_name = clean_name, progress = progress)
+ })
}
--- a/src/Pure/Tools/scala_build.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/scala_build.scala Fri Apr 01 23:19:12 2022 +0200
@@ -99,13 +99,13 @@
}
def build_result(dir: Path, component: Boolean = false): Result = {
- Isabelle_System.with_tmp_file("result", "jar")(tmp_file => {
+ Isabelle_System.with_tmp_file("result", "jar") { tmp_file =>
val output =
build(dir, component = component, no_title = true, do_build = true, module = Some(tmp_file))
val jar_bytes = Bytes.read(tmp_file)
val jar_path = context(dir, component = component).module_result
Result(output, jar_bytes, jar_path)
- })
+ }
}
def component_contexts(): List[Context] =
--- a/src/Pure/Tools/scala_project.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/scala_project.scala Fri Apr 01 23:19:12 2022 +0200
@@ -258,13 +258,13 @@
val isabelle_tool =
Isabelle_Tool("scala_project", "setup IDE project for Isabelle/Java/Scala sources",
Scala_Project.here,
- args => {
- var build_tool: Option[Build_Tool] = None
- var project_dir = default_project_dir
- var symlinks = false
- var force = false
+ { args =>
+ var build_tool: Option[Build_Tool] = None
+ var project_dir = default_project_dir
+ var symlinks = false
+ var force = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle scala_project [OPTIONS] [MORE_SOURCES ...]
Options are:
@@ -278,22 +278,22 @@
as IntelliJ IDEA. Either option -G or -M is mandatory to specify the
build tool.
""",
- "D:" -> (arg => project_dir = Path.explode(arg)),
- "G" -> (_ => build_tool = Some(Gradle)),
- "L" -> (_ => symlinks = true),
- "M" -> (_ => build_tool = Some(Maven)),
- "f" -> (_ => force = true))
+ "D:" -> (arg => project_dir = Path.explode(arg)),
+ "G" -> (_ => build_tool = Some(Gradle)),
+ "L" -> (_ => symlinks = true),
+ "M" -> (_ => build_tool = Some(Maven)),
+ "f" -> (_ => force = true))
- val more_args = getopts(args)
+ val more_args = getopts(args)
- val more_sources = more_args.map(Path.explode)
- val progress = new Console_Progress
+ val more_sources = more_args.map(Path.explode)
+ val progress = new Console_Progress
- if (build_tool.isEmpty) {
- error("Unspecified build tool: need to provide option -G or -M")
- }
+ if (build_tool.isEmpty) {
+ error("Unspecified build tool: need to provide option -G or -M")
+ }
- scala_project(build_tool.get, project_dir = project_dir, more_sources = more_sources,
- symlinks = symlinks, force = force, progress = progress)
- })
+ scala_project(build_tool.get, project_dir = project_dir, more_sources = more_sources,
+ symlinks = symlinks, force = force, progress = progress)
+ })
}
--- a/src/Pure/Tools/server.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/server.scala Fri Apr 01 23:19:12 2022 +0200
@@ -340,13 +340,13 @@
def active: Boolean =
try {
- using(connection())(connection => {
+ using(connection()) { connection =>
connection.set_timeout(Time.seconds(2.0))
connection.read_line_message() match {
case Some(Reply(Reply.OK, _)) => true
case _ => false
}
- })
+ }
}
catch {
case _: IOException => false
@@ -389,36 +389,36 @@
existing_server: Boolean = false,
log: Logger = No_Logger
): (Info, Option[Server]) = {
- using(SQLite.open_database(Data.database))(db => {
- db.transaction {
- 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")
+ using(SQLite.open_database(Data.database)) { db =>
+ db.transaction {
+ 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)
+ 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()
- })
+ 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))
- }
+ server.start()
+ (server_info, Some(server))
}
- })
+ }
+ }
}
def exit(name: String = default_name): Boolean = {
@@ -439,17 +439,16 @@
val isabelle_tool =
Isabelle_Tool("server", "manage resident Isabelle servers", Scala_Project.here,
- 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
+ { 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("""
+ val getopts = Getopts("""
Usage: isabelle server [OPTIONS]
Options are:
@@ -471,30 +470,30 @@
"s" -> (_ => existing_server = true),
"x" -> (_ => operation_exit = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ 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) Process_Result.RC.ok else Process_Result.RC.failure)
- }
- 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())
+ 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) Process_Result.RC.ok else Process_Result.RC.failure)
}
- server.foreach(_.join())
- }
- })
+ 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(port0: Int, val log: Logger) extends Server.Handler(port0) {
@@ -528,7 +527,7 @@
override def join(): Unit = { super.join(); shutdown() }
override def handle(connection: Server.Connection): Unit = {
- using(new Server.Context(server, connection))(context => {
+ using(new Server.Context(server, connection)) { context =>
connection.reply_ok(
JSON.Object(
"isabelle_id" -> Isabelle_System.isabelle_id(),
@@ -570,6 +569,6 @@
}
}
}
- })
+ }
}
}
--- a/src/Pure/Tools/server_commands.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/server_commands.scala Fri Apr 01 23:19:12 2022 +0200
@@ -88,7 +88,7 @@
"ok" -> results.ok,
"return_code" -> results.rc,
"sessions" ->
- results.sessions.toList.sortBy(sessions_order).map(session => {
+ results.sessions.toList.sortBy(sessions_order).map { session =>
val result = results(session)
JSON.Object(
"session" -> session,
@@ -96,7 +96,7 @@
"return_code" -> result.rc,
"timeout" -> result.timeout,
"timing" -> result.timing.json)
- }))
+ })
if (results.ok) (results_json, results, options, base_info)
else {
@@ -147,12 +147,12 @@
override val command_body: Server.Command_Body =
{ case (context, Session_Start(args)) =>
- context.make_task(task => {
+ context.make_task { task =>
val (res, entry) =
Session_Start.command(args, progress = task.progress, log = context.server.log)
context.server.add_session(entry)
res
- })
+ }
}
}
@@ -277,10 +277,10 @@
override val command_body: Server.Command_Body =
{ case (context, Use_Theories(args)) =>
- context.make_task(task => {
- val session = context.server.the_session(args.session_id)
- Use_Theories.command(args, session, id = task.id, progress = task.progress)._1
- })
+ context.make_task { task =>
+ val session = context.server.the_session(args.session_id)
+ Use_Theories.command(args, session, id = task.id, progress = task.progress)._1
+ }
}
}
--- a/src/Pure/Tools/simplifier_trace.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala Fri Apr 01 23:19:12 2022 +0200
@@ -162,7 +162,7 @@
}
Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)(
- consume = (arg: Any) => {
+ consume = { (arg: Any) =>
arg match {
case Handle_Results(session, id, results, slot) =>
var new_context = contexts.getOrElse(id, Context())
--- a/src/Pure/Tools/update.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/update.scala Fri Apr 01 23:19:12 2022 +0200
@@ -37,7 +37,7 @@
case t => List(t)
}
- context.sessions(logic, log = log).foreach(_.process((args: Dump.Args) => {
+ context.sessions(logic, log = log).foreach(_.process { (args: Dump.Args) =>
progress.echo("Processing theory " + args.print_node + " ...")
val snapshot = args.snapshot
@@ -53,7 +53,7 @@
File.write(node_name.path, source1)
}
}
- }))
+ })
context.check_errors
}
@@ -63,20 +63,20 @@
val isabelle_tool =
Isabelle_Tool("update", "update theory sources based on PIDE markup", Scala_Project.here,
- args => {
- var base_sessions: List[String] = Nil
- var select_dirs: List[Path] = Nil
- var requirements = false
- var exclude_session_groups: List[String] = Nil
- var all_sessions = false
- var dirs: List[Path] = Nil
- var session_groups: List[String] = Nil
- var logic = Dump.default_logic
- var options = Options.init()
- var verbose = false
- var exclude_sessions: List[String] = Nil
+ { args =>
+ var base_sessions: List[String] = Nil
+ var select_dirs: List[Path] = Nil
+ var requirements = false
+ var exclude_session_groups: List[String] = Nil
+ var all_sessions = false
+ var dirs: List[Path] = Nil
+ var session_groups: List[String] = Nil
+ var logic = Dump.default_logic
+ var options = Options.init()
+ var verbose = false
+ var exclude_sessions: List[String] = Nil
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle update [OPTIONS] [SESSIONS ...]
Options are:
@@ -95,36 +95,36 @@
Update theory sources based on PIDE markup.
""",
- "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
- "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
- "R" -> (_ => requirements = true),
- "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
- "a" -> (_ => all_sessions = true),
- "b:" -> (arg => logic = arg),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "g:" -> (arg => session_groups = session_groups ::: List(arg)),
- "o:" -> (arg => options = options + arg),
- "u:" -> (arg => options = options + ("update_" + arg)),
- "v" -> (_ => verbose = true),
- "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+ "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
+ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "R" -> (_ => requirements = true),
+ "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+ "a" -> (_ => all_sessions = true),
+ "b:" -> (arg => logic = arg),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+ "o:" -> (arg => options = options + arg),
+ "u:" -> (arg => options = options + ("update_" + arg)),
+ "v" -> (_ => verbose = true),
+ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
- val sessions = getopts(args)
+ val sessions = getopts(args)
- val progress = new Console_Progress(verbose = verbose)
+ val progress = new Console_Progress(verbose = verbose)
- progress.interrupt_handler {
- update(options, logic,
- progress = progress,
- dirs = dirs,
- select_dirs = select_dirs,
- selection = Sessions.Selection(
- requirements = requirements,
- all_sessions = all_sessions,
- base_sessions = base_sessions,
- exclude_session_groups = exclude_session_groups,
- exclude_sessions = exclude_sessions,
- session_groups = session_groups,
- sessions = sessions))
- }
- })
+ progress.interrupt_handler {
+ update(options, logic,
+ progress = progress,
+ dirs = dirs,
+ select_dirs = select_dirs,
+ selection = Sessions.Selection(
+ requirements = requirements,
+ all_sessions = all_sessions,
+ base_sessions = base_sessions,
+ exclude_session_groups = exclude_session_groups,
+ exclude_sessions = exclude_sessions,
+ session_groups = session_groups,
+ sessions = sessions))
+ }
+ })
}
--- a/src/Pure/Tools/update_cartouches.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/update_cartouches.scala Fri Apr 01 23:19:12 2022 +0200
@@ -75,10 +75,10 @@
val isabelle_tool =
Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches",
Scala_Project.here,
- args => {
- var replace_text = false
+ { args =>
+ var replace_text = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle update_cartouches [FILES|DIRS...]
Options are:
@@ -89,15 +89,15 @@
Old versions of files are preserved by appending "~~".
""",
- "t" -> (_ => replace_text = true))
+ "t" -> (_ => replace_text = true))
- val specs = getopts(args)
- if (specs.isEmpty) getopts.usage()
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
- for {
- spec <- specs
- file <- File.find_files(Path.explode(spec).file,
- file => file.getName.endsWith(".thy") || file.getName == "ROOT")
- } update_cartouches(replace_text, File.path(file))
- })
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file,
+ file => file.getName.endsWith(".thy") || file.getName == "ROOT")
+ } update_cartouches(replace_text, File.path(file))
+ })
}
--- a/src/Pure/Tools/update_comments.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/update_comments.scala Fri Apr 01 23:19:12 2022 +0200
@@ -46,8 +46,8 @@
val isabelle_tool =
Isabelle_Tool("update_comments", "update formal comments in outer syntax",
Scala_Project.here,
- args => {
- val getopts = Getopts("""
+ { args =>
+ val getopts = Getopts("""
Usage: isabelle update_comments [FILES|DIRS...]
Recursively find .thy files and update formal comments in outer syntax.
@@ -55,12 +55,12 @@
Old versions of files are preserved by appending "~~".
""")
- val specs = getopts(args)
- if (specs.isEmpty) getopts.usage()
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
- for {
- spec <- specs
- file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_comments(File.path(file))
- })
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+ } update_comments(File.path(file))
+ })
}
--- a/src/Pure/Tools/update_header.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/update_header.scala Fri Apr 01 23:19:12 2022 +0200
@@ -29,10 +29,10 @@
val isabelle_tool =
Isabelle_Tool("update_header", "replace obsolete theory header command",
Scala_Project.here,
- args => {
- var section = "section"
+ { args =>
+ var section = "section"
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle update_header [FILES|DIRS...]
Options are:
@@ -44,17 +44,17 @@
Old versions of files are preserved by appending "~~".
""",
- "s:" -> (arg => section = arg))
+ "s:" -> (arg => section = arg))
- val specs = getopts(args)
- if (specs.isEmpty) getopts.usage()
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
- if (!headings.contains(section))
- error("Bad heading command: " + quote(section))
+ if (!headings.contains(section))
+ error("Bad heading command: " + quote(section))
- for {
- spec <- specs
- file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_header(section, File.path(file))
- })
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+ } update_header(section, File.path(file))
+ })
}
--- a/src/Pure/Tools/update_then.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/update_then.scala Fri Apr 01 23:19:12 2022 +0200
@@ -30,8 +30,9 @@
val isabelle_tool =
Isabelle_Tool("update_then", "expand old Isar command conflations 'hence' and 'thus'",
- Scala_Project.here, args => {
- val getopts = Getopts("""
+ Scala_Project.here,
+ { args =>
+ val getopts = Getopts("""
Usage: isabelle update_then [FILES|DIRS...]
Recursively find .thy files and expand old Isar command conflations:
@@ -42,12 +43,12 @@
Old versions of files are preserved by appending "~~".
""")
- val specs = getopts(args)
- if (specs.isEmpty) getopts.usage()
-
- for {
- spec <- specs
- file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_then(File.path(file))
- })
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
+
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+ } update_then(File.path(file))
+ })
}
--- a/src/Pure/Tools/update_theorems.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Pure/Tools/update_theorems.scala Fri Apr 01 23:19:12 2022 +0200
@@ -30,8 +30,9 @@
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords",
- Scala_Project.here, args => {
- val getopts = Getopts("""
+ Scala_Project.here,
+ { args =>
+ val getopts = Getopts("""
Usage: isabelle update_theorems [FILES|DIRS...]
Recursively find .thy files and update toplevel theorem keywords:
@@ -44,12 +45,12 @@
Old versions of files are preserved by appending "~~".
""")
- val specs = getopts(args)
- if (specs.isEmpty) getopts.usage()
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
- for {
- spec <- specs
- file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_theorems(File.path(file))
- })
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+ } update_theorems(File.path(file))
+ })
}
--- a/src/Tools/Graphview/graph_file.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/Graphview/graph_file.scala Fri Apr 01 23:19:12 2022 +0200
@@ -42,8 +42,8 @@
}
def make_pdf(options: Options, graph: Graph_Display.Graph): Bytes =
- Isabelle_System.with_tmp_file("graph", ext = "pdf")(graph_file => {
+ Isabelle_System.with_tmp_file("graph", ext = "pdf") { graph_file =>
write(options, graph_file.file, graph)
Bytes.read(graph_file)
- })
+ }
}
--- a/src/Tools/Graphview/layout.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/Graphview/layout.scala Fri Apr 01 23:19:12 2022 +0200
@@ -195,7 +195,7 @@
levels: List[Level]
): List[Level] = {
def resort(parent: Level, child: Level, top_down: Boolean): Level =
- child.map(v => {
+ child.map({ v =>
val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
val weight =
ps.foldLeft(0.0) { case (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
--- a/src/Tools/Graphview/mutator.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/Graphview/mutator.scala Fri Apr 01 23:19:12 2022 +0200
@@ -152,7 +152,7 @@
extends Graph_Mutator(
"Add transitive closure",
"Adds all family members of all current nodes.",
- (full_graph, graph) => {
+ { (full_graph, graph) =>
val withparents =
if (parents) add_node_group(full_graph, graph, full_graph.all_preds(graph.keys))
else graph
--- a/src/Tools/Graphview/mutator_dialog.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/Graphview/mutator_dialog.scala Fri Apr 01 23:19:12 2022 +0200
@@ -88,10 +88,10 @@
def paint_panels(): Unit = {
Focus_Traveral_Policy.clear()
filter_panel.contents.clear()
- panels.map(x => {
- filter_panel.contents += x
- Focus_Traveral_Policy.addAll(x.focusList)
- })
+ panels.map { x =>
+ filter_panel.contents += x
+ Focus_Traveral_Policy.addAll(x.focusList)
+ }
filter_panel.contents += Swing.VGlue
Focus_Traveral_Policy.add(mutator_box.peer.asInstanceOf[java.awt.Component])
--- a/src/Tools/VSCode/src/build_vscode_extension.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala Fri Apr 01 23:19:12 2022 +0200
@@ -157,7 +157,7 @@
/* build */
val vsix_name =
- Isabelle_System.with_tmp_dir("build")(build_dir => {
+ Isabelle_System.with_tmp_dir("build") { build_dir =>
val manifest_text = File.read(VSCode_Main.extension_dir + VSCode_Main.MANIFEST)
val manifest_entries = split_lines(manifest_text).filter(_.nonEmpty)
val manifest_shasum: String = {
@@ -185,7 +185,7 @@
Isabelle_System.copy_file(build_dir + Path.basic(vsix_name), component_dir)
vsix_name
- })
+ }
/* settings */
@@ -215,12 +215,12 @@
val isabelle_tool =
Isabelle_Tool("build_vscode_extension", "build Isabelle/VSCode extension module",
Scala_Project.here,
- args => {
- var target_dir = Path.current
- var dirs: List[Path] = Nil
- var logic = default_logic
+ { args =>
+ var target_dir = Path.current
+ var dirs: List[Path] = Nil
+ var logic = default_logic
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build_vscode_extension
Options are:
@@ -231,17 +231,17 @@
Build the Isabelle/VSCode extension as component, for inclusion into the
local VSCodium configuration.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "l:" -> (arg => logic = arg))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "l:" -> (arg => logic = arg))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val options = Options.init()
- val progress = new Console_Progress()
+ val options = Options.init()
+ val progress = new Console_Progress()
- build_extension(options, target_dir = target_dir, logic = logic, dirs = dirs,
- progress = progress)
- })
+ build_extension(options, target_dir = target_dir, logic = logic, dirs = dirs,
+ progress = progress)
+ })
}
--- a/src/Tools/VSCode/src/build_vscodium.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/VSCode/src/build_vscodium.scala Fri Apr 01 23:19:12 2022 +0200
@@ -71,7 +71,7 @@
def download(dir: Path, progress: Progress = new Progress): Unit = {
if (download_zip) Isabelle_System.require_command("unzip", test = "-h")
- Isabelle_System.with_tmp_file("download")(download_file => {
+ Isabelle_System.with_tmp_file("download") { download_file =>
Isabelle_System.download_file(vscodium_download + "/" + version + "/" + download_name,
download_file, progress = progress)
@@ -82,7 +82,7 @@
else {
Isabelle_System.gnutar("-xzf " + File.bash_path(download_file), dir = dir).check
}
- })
+ }
}
def get_vscodium_repository(build_dir: Path, progress: Progress = new Progress): Unit = {
@@ -189,7 +189,7 @@
}
def setup_node(target_dir: Path, progress: Progress): Unit = {
- Isabelle_System.with_tmp_dir("download")(download_dir => {
+ Isabelle_System.with_tmp_dir("download") { download_dir =>
download(download_dir, progress = progress)
val dir1 = init_resources(download_dir)
val dir2 = init_resources(target_dir)
@@ -198,7 +198,7 @@
Isabelle_System.rm_tree(dir2 + path)
Isabelle_System.copy_dir(dir1 + path, dir2 + path)
}
- })
+ }
}
def setup_electron(dir: Path): Unit = {
@@ -220,11 +220,10 @@
if (platform == Platform.Family.windows) {
val files =
- File.find_files(dir.file, pred = file =>
- {
- val name = file.getName
- name.endsWith(".dll") || name.endsWith(".exe") || name.endsWith(".node")
- })
+ File.find_files(dir.file, pred = { file =>
+ val name = file.getName
+ name.endsWith(".dll") || name.endsWith(".exe") || name.endsWith(".node")
+ })
files.foreach(file => File.set_executable(File.path(file), true))
Isabelle_System.bash("chmod -R o-w " + File.bash_path(dir)).check
}
@@ -291,7 +290,7 @@
val platform_info = linux_platform_info
check_system(List(platform_info.platform))
- Isabelle_System.with_tmp_dir("build")(build_dir => {
+ Isabelle_System.with_tmp_dir("build") { build_dir =>
platform_info.get_vscodium_repository(build_dir, progress = progress)
val vscode_dir = build_dir + Path.explode("vscode")
progress.echo("Prepare ...")
@@ -307,7 +306,7 @@
Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base,
diff_options = "--exclude=.git --exclude=node_modules")
}
- })
+ }
}
@@ -348,7 +347,7 @@
for (platform <- platforms) yield {
val platform_info = the_platform_info(platform)
- Isabelle_System.with_tmp_dir("build")(build_dir => {
+ Isabelle_System.with_tmp_dir("build") { build_dir =>
progress.echo("\n* Building " + platform + ":")
platform_info.get_vscodium_repository(build_dir, progress = progress)
@@ -377,7 +376,7 @@
platform_dir + resources)
platform_info.setup_executables(platform_dir)
- })
+ }
}
Isabelle_System.bash("gzip *.patch", cwd = patches_dir.file).check
@@ -422,12 +421,12 @@
val isabelle_tool1 =
Isabelle_Tool("build_vscodium", "build component for VSCodium",
Scala_Project.here,
- args => {
- var target_dir = Path.current
- var platforms = default_platforms
- var verbose = false
+ { args =>
+ var target_dir = Path.current
+ var platforms = default_platforms
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: build_vscodium [OPTIONS]
Options are:
@@ -440,26 +439,26 @@
The build platform needs to be Linux with nodejs/yarn, jq, and wine
for targeting Windows.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)),
- "v" -> (_ => verbose = true))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
+ val progress = new Console_Progress()
- build_vscodium(target_dir = target_dir, platforms = platforms,
- verbose = verbose, progress = progress)
- })
+ build_vscodium(target_dir = target_dir, platforms = platforms,
+ verbose = verbose, progress = progress)
+ })
val isabelle_tool2 =
Isabelle_Tool("vscode_patch", "patch VSCode source tree",
Scala_Project.here,
- args => {
- var base_dir = Path.current
+ { args =>
+ var base_dir = Path.current
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: vscode_patch [OPTIONS]
Options are:
@@ -467,12 +466,12 @@
Patch original VSCode source tree for use with Isabelle/VSCode.
""",
- "D:" -> (arg => base_dir = Path.explode(arg)))
+ "D:" -> (arg => base_dir = Path.explode(arg)))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val platform_info = the_platform_info(Platform.family)
- platform_info.patch_sources(base_dir)
- })
+ val platform_info = the_platform_info(Platform.family)
+ platform_info.patch_sources(base_dir)
+ })
}
--- a/src/Tools/VSCode/src/language_server.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Fri Apr 01 23:19:12 2022 +0200
@@ -29,20 +29,20 @@
val isabelle_tool =
Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", Scala_Project.here,
- args => {
- try {
- var logic_ancestor: Option[String] = None
- var log_file: Option[Path] = None
- var logic_requirements = false
- var dirs: List[Path] = Nil
- var include_sessions: List[String] = Nil
- var logic = default_logic
- var modes: List[String] = Nil
- var no_build = false
- var options = Options.init()
- var verbose = false
+ { args =>
+ try {
+ var logic_ancestor: Option[String] = None
+ var log_file: Option[Path] = None
+ var logic_requirements = false
+ var dirs: List[Path] = Nil
+ var include_sessions: List[String] = Nil
+ var logic = default_logic
+ var modes: List[String] = Nil
+ var no_build = false
+ var options = Options.init()
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle vscode_server [OPTIONS]
Options are:
@@ -59,43 +59,43 @@
Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
""",
- "A:" -> (arg => logic_ancestor = Some(arg)),
- "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
- "R:" -> (arg => { logic = arg; logic_requirements = true }),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
- "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
- "l:" -> (arg => logic = arg),
- "m:" -> (arg => modes = arg :: modes),
- "n" -> (_ => no_build = true),
- "o:" -> (arg => options = options + arg),
- "v" -> (_ => verbose = true))
+ "A:" -> (arg => logic_ancestor = Some(arg)),
+ "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
+ "R:" -> (arg => { logic = arg; logic_requirements = true }),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
+ "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
+ "l:" -> (arg => logic = arg),
+ "m:" -> (arg => modes = arg :: modes),
+ "n" -> (_ => no_build = true),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val log = Logger.make(log_file)
- val channel = new Channel(System.in, System.out, log, verbose)
- val server =
- new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
- include_sessions = include_sessions, session_ancestor = logic_ancestor,
- session_requirements = logic_requirements, session_no_build = no_build,
- modes = modes, log = log)
+ val log = Logger.make(log_file)
+ val channel = new Channel(System.in, System.out, log, verbose)
+ val server =
+ new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
+ include_sessions = include_sessions, session_ancestor = logic_ancestor,
+ session_requirements = logic_requirements, session_no_build = no_build,
+ modes = modes, log = log)
- // prevent spurious garbage on the main protocol channel
- val orig_out = System.out
- try {
- System.setOut(new PrintStream(new OutputStream { def write(n: Int): Unit = {} }))
- server.start()
+ // prevent spurious garbage on the main protocol channel
+ val orig_out = System.out
+ try {
+ System.setOut(new PrintStream(new OutputStream { def write(n: Int): Unit = {} }))
+ server.start()
+ }
+ finally { System.setOut(orig_out) }
}
- finally { System.setOut(orig_out) }
- }
- catch {
- case exn: Throwable =>
- val channel = new Channel(System.in, System.out, No_Logger)
- channel.error_message(Exn.message(exn))
- throw(exn)
- }
- })
+ catch {
+ case exn: Throwable =>
+ val channel = new Channel(System.in, System.out, No_Logger)
+ channel.error_message(Exn.message(exn))
+ throw(exn)
+ }
+ })
}
class Language_Server(
--- a/src/Tools/VSCode/src/preview_panel.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/VSCode/src/preview_panel.scala Fri Apr 01 23:19:12 2022 +0200
@@ -19,7 +19,7 @@
pending.change(map => map + (file -> column))
def flush(channel: Channel): Boolean = {
- pending.change_result(map => {
+ pending.change_result { map =>
val map1 =
map.iterator.foldLeft(map) {
case (m, (file, column)) =>
@@ -43,6 +43,6 @@
}
}
(map1.nonEmpty, map1)
- })
+ }
}
}
--- a/src/Tools/VSCode/src/vscode_main.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/VSCode/src/vscode_main.scala Fri Apr 01 23:19:12 2022 +0200
@@ -167,25 +167,25 @@
val isabelle_tool =
Isabelle_Tool("vscode", "Isabelle/VSCode interface wrapper", Scala_Project.here,
- args => {
- var logic_ancestor = ""
- var console = false
- var edit_extension = false
- var server_log = false
- var logic_requirements = false
- var uninstall = false
- var vsix_path = default_vsix_path
- var session_dirs = List.empty[Path]
- var include_sessions = List.empty[String]
- var logic = ""
- var modes = List.empty[String]
- var no_build = false
- var options = List.empty[String]
- var verbose = false
+ { args =>
+ var logic_ancestor = ""
+ var console = false
+ var edit_extension = false
+ var server_log = false
+ var logic_requirements = false
+ var uninstall = false
+ var vsix_path = default_vsix_path
+ var session_dirs = List.empty[Path]
+ var include_sessions = List.empty[String]
+ var logic = ""
+ var modes = List.empty[String]
+ var no_build = false
+ var options = List.empty[String]
+ var verbose = false
- def add_option(opt: String): Unit = options = options ::: List(opt)
+ def add_option(opt: String): Unit = options = options ::: List(opt)
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle vscode [OPTIONS] [ARGUMENTS] [-- VSCODE_OPTIONS]
-A NAME ancestor session for option -R (default: parent)
@@ -213,43 +213,43 @@
The following initial settings are provided for a fresh installation:
""" + default_settings,
- "A:" -> (arg => logic_ancestor = arg),
- "C" -> (_ => console = true),
- "E" -> (_ => edit_extension = true),
- "L" -> (_ => server_log = true),
- "R:" -> (arg => { logic = arg; logic_requirements = true }),
- "U" -> (_ => uninstall = true),
- "V:" -> (arg => vsix_path = Path.explode(arg)),
- "d:" -> (arg => session_dirs = session_dirs ::: List(Path.explode(arg))),
- "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
- "l:" -> (arg => { logic = arg; logic_requirements = false }),
- "m:" -> (arg => modes = modes ::: List(arg)),
- "n" -> (_ => no_build = true),
- "o:" -> add_option,
- "p:" -> (arg => add_option("ML_process_policy=" + arg)),
- "s" -> (_ => add_option("system_heaps=true")),
- "u" -> (_ => add_option("system_heaps=false")),
- "v" -> (_ => verbose = true))
+ "A:" -> (arg => logic_ancestor = arg),
+ "C" -> (_ => console = true),
+ "E" -> (_ => edit_extension = true),
+ "L" -> (_ => server_log = true),
+ "R:" -> (arg => { logic = arg; logic_requirements = true }),
+ "U" -> (_ => uninstall = true),
+ "V:" -> (arg => vsix_path = Path.explode(arg)),
+ "d:" -> (arg => session_dirs = session_dirs ::: List(Path.explode(arg))),
+ "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
+ "l:" -> (arg => { logic = arg; logic_requirements = false }),
+ "m:" -> (arg => modes = modes ::: List(arg)),
+ "n" -> (_ => no_build = true),
+ "o:" -> add_option,
+ "p:" -> (arg => add_option("ML_process_policy=" + arg)),
+ "s" -> (_ => add_option("system_heaps=true")),
+ "u" -> (_ => add_option("system_heaps=false")),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
+ val more_args = getopts(args)
- init_settings()
+ init_settings()
- val console_progress = new Console_Progress
+ val console_progress = new Console_Progress
- if (uninstall) uninstall_extension(progress = console_progress)
- else install_extension(vsix_path = vsix_path, progress = console_progress)
+ if (uninstall) uninstall_extension(progress = console_progress)
+ else install_extension(vsix_path = vsix_path, progress = console_progress)
- val (background, app_progress) =
- if (console) (false, console_progress)
- else { run_vscodium(List("--version")).check; (true, new Progress) }
+ val (background, app_progress) =
+ if (console) (false, console_progress)
+ else { run_vscodium(List("--version")).check; (true, new Progress) }
- run_vscodium(
- more_args ::: (if (edit_extension) List(File.platform_path(extension_dir)) else Nil),
- options = options, logic = logic, logic_ancestor = logic_ancestor,
- logic_requirements = logic_requirements, session_dirs = session_dirs,
- include_sessions = include_sessions, modes = modes, no_build = no_build,
- server_log = server_log, verbose = verbose, background = background,
- progress = app_progress).check
- })
+ run_vscodium(
+ more_args ::: (if (edit_extension) List(File.platform_path(extension_dir)) else Nil),
+ options = options, logic = logic, logic_ancestor = logic_ancestor,
+ logic_requirements = logic_requirements, session_dirs = session_dirs,
+ include_sessions = include_sessions, modes = modes, no_build = no_build,
+ server_log = server_log, verbose = verbose, background = background,
+ progress = app_progress).check
+ })
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Apr 01 23:19:12 2022 +0200
@@ -156,12 +156,12 @@
text: String,
range: Option[Line.Range] = None
): Unit = {
- state.change(st => {
+ state.change { st =>
val model = st.models.getOrElse(file, VSCode_Model.init(session, editor, node_name(file)))
val model1 =
(model.change_text(text, range) getOrElse model).set_version(version).external(false)
st.update_models(Some(file -> model1))
- })
+ }
}
def close_model(file: JFile): Boolean =
@@ -172,7 +172,7 @@
})
def sync_models(changed_files: Set[JFile]): Unit =
- state.change(st => {
+ state.change { st =>
val changed_models =
(for {
(file, model) <- st.models.iterator
@@ -181,7 +181,7 @@
model1 <- model.change_text(text)
} yield (file, model1)).toList
st.update_models(changed_models)
- })
+ }
/* overlays */
@@ -203,7 +203,7 @@
editor: Language_Server.Editor,
file_watcher: File_Watcher
): (Boolean, Boolean) = {
- state.change_result(st => {
+ state.change_result { st =>
/* theory files */
val thys =
@@ -252,14 +252,14 @@
val invoke_load = stable_tip_version.isEmpty
((invoke_input, invoke_load), st.update_models(loaded_models))
- })
+ }
}
/* pending input */
def flush_input(session: Session, channel: Channel): Unit = {
- state.change(st => {
+ state.change { st =>
val changed_models =
(for {
file <- st.pending_input.iterator
@@ -276,7 +276,7 @@
st.copy(
models = st.models ++ changed_models.iterator.map(_._2),
pending_input = Set.empty)
- })
+ }
}
@@ -290,7 +290,7 @@
(for ((file, model) <- st.models.iterator if model.node_visible) yield file)))
def flush_output(channel: Channel): Boolean = {
- state.change_result(st => {
+ state.change_result { st =>
val (postponed, flushed) =
(for {
file <- st.pending_output.iterator
@@ -317,7 +317,7 @@
st.copy(
models = st.models ++ changed_iterator,
pending_output = postponed.map(_._1).toSet))
- })
+ }
}
--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Fri Apr 01 23:19:12 2022 +0200
@@ -187,7 +187,7 @@
snapshot.version, command, Command.Markup_Index.markup,
command.range, Markup.Elements.full)
Isabelle_Sidekick.swing_markup_tree(markup, data.root,
- (info: Text.Info[List[XML.Elem]]) => {
+ { (info: Text.Info[List[XML.Elem]]) =>
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString
--- a/src/Tools/jEdit/jedit_main/scala_console.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala Fri Apr 01 23:19:12 2022 +0200
@@ -89,7 +89,7 @@
private class Interpreter {
private val running = Synchronized[Option[Thread]](None)
- def interrupt(): Unit = running.change(opt => { opt.foreach(_.interrupt()); opt })
+ def interrupt(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt })
private val interp =
Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
--- a/src/Tools/jEdit/src/completion_popup.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Apr 01 23:19:12 2022 +0200
@@ -594,7 +594,7 @@
val inner_key_listener: KeyListener =
JEdit_Lib.key_listener(
- key_pressed = (e: KeyEvent) => {
+ key_pressed = { (e: KeyEvent) =>
if (!e.isConsumed) {
e.getKeyCode match {
case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
--- a/src/Tools/jEdit/src/document_model.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Fri Apr 01 23:19:12 2022 +0200
@@ -114,7 +114,7 @@
/* sync external files */
def sync_files(changed_files: Set[JFile]): Boolean = {
- state.change_result(st => {
+ state.change_result { st =>
val changed_models =
(for {
(node_name, model) <- st.file_models_iterator
@@ -128,7 +128,7 @@
}).toList
if (changed_models.isEmpty) (false, st)
else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _)))
- })
+ }
}
@@ -225,7 +225,7 @@
def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) = {
GUI_Thread.require {}
- state.change_result(st => {
+ state.change_result { st =>
val doc_blobs = st.document_blobs
val buffer_edits =
@@ -270,7 +270,7 @@
} yield file.getParentFile).toSet)
((doc_blobs, model_edits ::: purge_edits), st1)
- })
+ }
}
--- a/src/Tools/jEdit/src/document_view.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Fri Apr 01 23:19:12 2022 +0200
@@ -175,9 +175,10 @@
private val key_listener =
JEdit_Lib.key_listener(
- key_pressed = (evt: KeyEvent) => {
- if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Isabelle.dismissed_popups(text_area.getView))
+ key_pressed = { (evt: KeyEvent) =>
+ if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Isabelle.dismissed_popups(text_area.getView)) {
evt.consume
+ }
}
)
--- a/src/Tools/jEdit/src/font_info.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/jEdit/src/font_info.scala Fri Apr 01 23:19:12 2022 +0200
@@ -54,7 +54,7 @@
// owned by GUI thread
private var steps = 0
private val delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
- change_size(size => {
+ change_size { size =>
var i = size.round
while (steps != 0 && i > 0) {
if (steps > 0) { i += (i / 10) max 1; steps -= 1 }
@@ -62,7 +62,7 @@
}
steps = 0
i.toFloat
- })
+ }
}
def step(i: Int): Unit = {
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Apr 01 23:19:12 2022 +0200
@@ -75,7 +75,7 @@
getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
- get_background().foreach(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
+ get_background().foreach { bg => getPainter.setBackground(bg); getGutter.setBackground(bg) }
getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
@@ -200,7 +200,7 @@
})
addKeyListener(JEdit_Lib.key_listener(
- key_pressed = (evt: KeyEvent) => {
+ key_pressed = { (evt: KeyEvent) =>
val strict_control =
JEdit_Lib.command_modifier(evt) && !JEdit_Lib.shift_modifier(evt)
@@ -222,7 +222,7 @@
}
if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
},
- key_typed = (evt: KeyEvent) => {
+ key_typed = { (evt: KeyEvent) =>
if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
})
)
--- a/src/Tools/jEdit/src/rich_text_area.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Apr 01 23:19:12 2022 +0200
@@ -79,13 +79,13 @@
private val key_listener =
JEdit_Lib.key_listener(
- key_pressed = (evt: KeyEvent) => {
+ key_pressed = { (evt: KeyEvent) =>
val mod = PIDE.options.string("jedit_focus_modifier")
val old = caret_focus_modifier
caret_focus_modifier = (mod.nonEmpty && mod == JEdit_Lib.modifier_string(evt))
if (caret_focus_modifier != old) caret_update()
},
- key_released = _ => {
+ key_released = { _ =>
if (caret_focus_modifier) {
caret_focus_modifier = false
caret_update()
--- a/src/Tools/jEdit/src/syntax_style.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala Fri Apr 01 23:19:12 2022 +0200
@@ -39,21 +39,20 @@
new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = {
- font_style(style, font0 =>
- {
- val font1 = font0.deriveFont(JMap.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
+ font_style(style, { font0 =>
+ val font1 = font0.deriveFont(JMap.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
- def shift(y: Float): Font =
- GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
+ def shift(y: Float): Font =
+ GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
- val m0 = GUI.line_metrics(font0)
- val m1 = GUI.line_metrics(font1)
- val a = m1.getAscent - m0.getAscent
- val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
- if (a > 0.0f) shift(a)
- else if (b > 0.0f) shift(- b)
- else font1
- })
+ val m0 = GUI.line_metrics(font0)
+ val m1 = GUI.line_metrics(font1)
+ val a = m1.getAscent - m0.getAscent
+ val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
+ if (a > 0.0f) shift(a)
+ else if (b > 0.0f) shift(- b)
+ else font1
+ })
}
private def bold_style(style: SyntaxStyle): SyntaxStyle =
@@ -176,14 +175,14 @@
result.toString
}
- text_area.getSelection.foreach(sel => {
+ text_area.getSelection.foreach { sel =>
val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
JEdit_Lib.get_text(buffer, before) match {
case Some(s) if HTML.is_control(s) =>
text_area.extendSelection(before.start, before.stop)
case _ =>
}
- })
+ }
text_area.getSelection.toList match {
case Nil =>
--- a/src/Tools/jEdit/src/text_overview.scala Fri Apr 01 17:06:10 2022 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala Fri Apr 01 23:19:12 2022 +0200
@@ -111,7 +111,7 @@
private def is_running(): Boolean = !future_refresh.value.is_finished
def invoke(): Unit = delay_refresh.invoke()
- def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel(); x }) }
+ def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change { x => x.cancel(); x } }
private val delay_refresh =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {