--- a/src/Pure/Admin/afp.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Admin/afp.scala Fri Mar 27 22:06:46 2020 +0100
@@ -166,7 +166,7 @@
/* dependency graph */
private def sessions_deps(entry: AFP.Entry): List[String] =
- entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
+ entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds).distinct.sorted
lazy val entries_graph: Graph[String, Unit] =
{
@@ -214,7 +214,7 @@
case 1 | 2 =>
val graph = sessions_structure.build_graph.restrict(sessions.toSet)
val force_part1 =
- graph.all_preds(graph.all_succs(AFP.force_partition1.filter(graph.defined(_)))).toSet
+ graph.all_preds(graph.all_succs(AFP.force_partition1.filter(graph.defined))).toSet
val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
if (n == 1) part1 else part2
case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
--- a/src/Pure/Admin/build_fonts.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Admin/build_fonts.scala Fri Mar 27 22:06:46 2020 +0100
@@ -284,7 +284,7 @@
val domain =
(for ((name, index) <- targets if index == 0)
yield Fontforge.font_domain(target_dir + hinted_path(false) + name))
- .flatten.toSet.toList.sorted
+ .flatten.distinct.sorted
Fontforge.execute(
Fontforge.commands(
--- a/src/Pure/Admin/build_history.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Admin/build_history.scala Fri Mar 27 22:06:46 2020 +0100
@@ -454,7 +454,7 @@
"B" -> (_ => multicore_base = true),
"C:" -> (arg => components_base = Path.explode(arg)),
"H:" -> (arg => heap = Some(Value.Int.parse(arg))),
- "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse(_))),
+ "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
"N:" -> (arg => isabelle_identifier = arg),
"P:" -> (arg => afp_partition = Value.Int.parse(arg)),
"U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
--- a/src/Pure/Admin/build_jdk.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Admin/build_jdk.scala Fri Mar 27 22:06:46 2020 +0100
@@ -106,7 +106,7 @@
}
val dir_entry =
- File.read_dir(tmp_dir).filterNot(suppress_name(_)) match {
+ File.read_dir(tmp_dir).filterNot(suppress_name) match {
case List(s) => s
case _ => error("Archive contains multiple directories")
}
@@ -144,7 +144,7 @@
val extracted = archives.map(extract_archive(dir, _))
val version =
- extracted.map(_._1).toSet.toList match {
+ extracted.map(_._1).distinct match {
case List(version) => version
case Nil => error("No archives")
case versions =>
@@ -232,7 +232,7 @@
val more_args = getopts(args)
if (more_args.isEmpty) getopts.usage()
- val archives = more_args.map(Path.explode(_))
+ val archives = more_args.map(Path.explode)
val progress = new Console_Progress()
build_jdk(archives = archives, progress = progress, target_dir = target_dir)
--- a/src/Pure/Admin/build_release.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Admin/build_release.scala Fri Mar 27 22:06:46 2020 +0100
@@ -163,7 +163,7 @@
terminate_lines("#bundled components" ::
(for {
(catalog, bundled) <- catalogs.iterator
- val path = Components.admin(dir) + Path.basic(catalog)
+ path = Components.admin(dir) + Path.basic(catalog)
if path.is_file
line <- split_lines(File.read(path))
if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
@@ -196,7 +196,7 @@
if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
else None
case _ => if (Bundled.detect(line)) None else Some(line)
- }) ::: more_names.map(contrib_name(_)))
+ }) ::: more_names.map(contrib_name))
}
def make_contrib(dir: Path)
@@ -428,7 +428,6 @@
val bundle_infos = platform_families.map(release.bundle_info)
for (bundle_info <- bundle_infos) {
- val bundle_archive = release.dist_dir + bundle_info.path
val isabelle_name = release.dist_name
val platform = bundle_info.platform
--- a/src/Pure/Admin/components.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Admin/components.scala Fri Mar 27 22:06:46 2020 +0100
@@ -38,7 +38,7 @@
/* component collections */
- val default_components_base = Path.explode("$ISABELLE_COMPONENTS_BASE")
+ val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
def admin(dir: Path): Path = dir + Path.explode("Admin/components")
@@ -125,7 +125,7 @@
case _ => error("Bad components.sha1 entry: " + quote(line))
})
- def write_components_sha1(entries: List[SHA1_Digest]) =
+ def write_components_sha1(entries: List[SHA1_Digest]): Unit =
File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n"))
--- a/src/Pure/Admin/isabelle_cronjob.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Mar 27 22:06:46 2020 +0100
@@ -18,14 +18,14 @@
/* global resources: owned by main cronjob */
val backup = "lxbroy10:cronjob"
- val main_dir = Path.explode("~/cronjob")
- val main_state_file = main_dir + Path.explode("run/main.state")
- val current_log = main_dir + Path.explode("run/main.log") // owned by log service
- val cumulative_log = main_dir + Path.explode("log/main.log") // owned by log service
+ val main_dir: Path = Path.explode("~/cronjob")
+ val main_state_file: Path = main_dir + Path.explode("run/main.state")
+ val current_log: Path = main_dir + Path.explode("run/main.log") // owned by log service
+ val cumulative_log: Path = main_dir + Path.explode("log/main.log") // owned by log service
val isabelle_repos_source = "https://isabelle.sketis.net/repos/isabelle"
- val isabelle_repos = main_dir + Path.explode("isabelle")
- val afp_repos = main_dir + Path.explode("AFP")
+ val isabelle_repos: Path = main_dir + Path.explode("isabelle")
+ val afp_repos: Path = main_dir + Path.explode("AFP")
val build_log_dirs =
List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
@@ -42,7 +42,7 @@
def get_rev(): String = Mercurial.repository(isabelle_repos).id()
def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
- val init =
+ val init: Logger_Task =
Logger_Task("init", logger =>
{
Isabelle_Devel.make_index()
@@ -61,7 +61,7 @@
Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath)
})
- val exit =
+ val exit: Logger_Task =
Logger_Task("exit", logger =>
{
Isabelle_System.bash(
@@ -72,7 +72,7 @@
/* build release */
- val build_release =
+ val build_release: Logger_Task =
Logger_Task("build_release", logger =>
{
Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev())
@@ -81,7 +81,7 @@
/* integrity test of build_history vs. build_history_base */
- val build_history_base =
+ val build_history_base: Logger_Task =
Logger_Task("build_history_base", logger =>
{
using(logger.ssh_context.open_session("lxbroy10"))(ssh =>
@@ -414,7 +414,7 @@
def shutdown() { thread.shutdown() }
- val hostname = Isabelle_System.hostname()
+ val hostname: String = Isabelle_System.hostname()
def log(date: Date, task_name: String, msg: String): Unit =
if (task_name != "")
--- a/src/Pure/Admin/isabelle_devel.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Admin/isabelle_devel.scala Fri Mar 27 22:06:46 2020 +0100
@@ -14,8 +14,8 @@
val BUILD_STATUS = "build_status"
val CRONJOB_LOG = "cronjob-main.log"
- val root = Path.explode("~/html-data/devel")
- val cronjob_log = root + Path.basic(CRONJOB_LOG)
+ val root: Path = Path.explode("~/html-data/devel")
+ val cronjob_log: Path = root + Path.basic(CRONJOB_LOG)
/* index */
--- a/src/Pure/Admin/jenkins.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Admin/jenkins.scala Fri Mar 27 22:06:46 2020 +0100
@@ -43,7 +43,7 @@
options: Options, job_names: List[String], dir: Path, progress: Progress = No_Progress)
{
val store = Sessions.store(options)
- val infos = job_names.flatMap(build_job_infos(_))
+ val infos = job_names.flatMap(build_job_infos)
Par_List.map((info: Job_Info) => info.download_log(store, dir, progress), infos)
}
@@ -106,7 +106,7 @@
Isabelle_System.mkdirs(log_dir)
val ml_statistics =
- session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
+ session_logs.map(_._1).distinct.sorted.flatMap(session_name =>
read_ml_statistics(store, session_name).
map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
--- a/src/Pure/Admin/other_isabelle.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Admin/other_isabelle.scala Fri Mar 27 22:06:46 2020 +0100
@@ -62,7 +62,7 @@
val etc_preferences: Path = etc + Path.explode("preferences")
def copy_fonts(target_dir: Path): Unit =
- Isabelle_Fonts.make_entries(getenv = getenv(_), hidden = true).
+ Isabelle_Fonts.make_entries(getenv = getenv, hidden = true).
foreach(entry => File.copy(entry.path, target_dir))
--- a/src/Pure/General/csv.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/csv.scala Fri Mar 27 22:06:46 2020 +0100
@@ -20,7 +20,7 @@
sealed case class Record(fields: Any*)
{
- override def toString: String = fields.iterator.map(print_field(_)).mkString(",")
+ override def toString: String = fields.iterator.map(print_field).mkString(",")
}
sealed case class File(name: String, header: List[String], records: List[Record])
--- a/src/Pure/General/date.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/date.scala Fri Mar 27 22:06:46 2020 +0100
@@ -33,7 +33,7 @@
}
def apply(pats: String*): Format =
- make(pats.toList.map(Date.Formatter.pattern(_)))
+ make(pats.toList.map(Date.Formatter.pattern))
val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
val date: Format = Format("dd-MMM-uuuu")
@@ -56,7 +56,7 @@
def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
pats.flatMap(pat => {
val fmt = pattern(pat)
- if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_))
+ if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale)
})
@tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,
--- a/src/Pure/General/exn.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/exn.scala Fri Mar 27 22:06:46 2020 +0100
@@ -70,7 +70,7 @@
def release_first[A](results: List[Result[A]]): List[A] =
results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
case Some(Exn(exn)) => throw exn
- case _ => results.map(release(_))
+ case _ => results.map(release)
}
--- a/src/Pure/General/file.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/file.scala Fri Mar 27 22:06:46 2020 +0100
@@ -213,7 +213,7 @@
val line =
try { reader.readLine}
catch { case _: IOException => null }
- if (line == null) None else Some(line)
+ Option(line)
}
def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
--- a/src/Pure/General/graph.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/graph.scala Fri Mar 27 22:06:46 2020 +0100
@@ -123,9 +123,9 @@
(Map.empty[Key, Long] /: xs)(reach(0))
}
def node_height(count: Key => Long): Map[Key, Long] =
- reachable_length(count, imm_preds(_), maximals)
+ reachable_length(count, imm_preds, maximals)
def node_depth(count: Key => Long): Map[Key, Long] =
- reachable_length(count, imm_succs(_), minimals)
+ reachable_length(count, imm_succs, minimals)
/*reachable nodes with size limit*/
def reachable_limit(
@@ -138,7 +138,7 @@
{
val (n, rs) = res
if (rs.contains(x)) res
- else ((n + count(x), rs + x) /: next(x))(reach _)
+ else ((n + count(x), rs + x) /: next(x))(reach)
}
@tailrec def reachs(size: Long, rs: Keys, rest: List[Key]): Keys =
--- a/src/Pure/General/json.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/json.scala Fri Mar 27 22:06:46 2020 +0100
@@ -9,6 +9,7 @@
package isabelle
+import scala.util.matching.Regex
import scala.util.parsing.combinator.Parsers
import scala.util.parsing.combinator.lexical.Scanners
import scala.util.parsing.input.CharArrayReader.EofCh
@@ -61,14 +62,14 @@
def errorToken(msg: String): Token = Token(Kind.ERROR, msg)
val white_space: String = " \t\n\r"
- override val whiteSpace = ("[" + white_space + "]+").r
+ override val whiteSpace: Regex = ("[" + white_space + "]+").r
def whitespace: Parser[Any] = many(character(white_space.contains(_)))
- val letter: Parser[String] = one(character(Symbol.is_ascii_letter(_)))
- val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter(_)))
+ val letter: Parser[String] = one(character(Symbol.is_ascii_letter))
+ val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter))
- def digits: Parser[String] = many(character(Symbol.is_ascii_digit(_)))
- def digits1: Parser[String] = many1(character(Symbol.is_ascii_digit(_)))
+ def digits: Parser[String] = many(character(Symbol.is_ascii_digit))
+ def digits1: Parser[String] = many1(character(Symbol.is_ascii_digit))
/* keyword */
@@ -114,8 +115,8 @@
one(character("eE".contains(_))) ~ maybe(character("-+".contains(_))) ~ digits1 ^^
{ case a ~ b ~ c => a + b + c }
- def zero = one(character(c => c == '0'))
- def nonzero = one(character(c => c != '0' && Symbol.is_ascii_digit(c)))
+ def zero: Parser[String] = one(character(c => c == '0'))
+ def nonzero: Parser[String] = one(character(c => c != '0' && Symbol.is_ascii_digit(c)))
def positive: Parser[String] = nonzero ~ digits ^^ { case a ~ b => a + b }
@@ -326,7 +327,7 @@
object Seconds
{
def unapply(json: T): Option[Time] =
- Double.unapply(json).map(Time.seconds(_))
+ Double.unapply(json).map(Time.seconds)
}
}
@@ -402,9 +403,9 @@
: Option[List[A]] = value_default(obj, name, Value.List.unapply(_, unapply), default)
def strings(obj: T, name: String): Option[List[String]] =
- list(obj, name, JSON.Value.String.unapply _)
+ list(obj, name, JSON.Value.String.unapply)
def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
- list_default(obj, name, JSON.Value.String.unapply _, default)
+ list_default(obj, name, JSON.Value.String.unapply, default)
def seconds(obj: T, name: String): Option[Time] =
value(obj, name, Value.Seconds.unapply)
--- a/src/Pure/General/linear_set.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/linear_set.scala Fri Mar 27 22:06:46 2020 +0100
@@ -17,7 +17,7 @@
object Linear_Set extends SetFactory[Linear_Set]
{
private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
- override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]]
+ override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]]
implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
def newBuilder[A]: Builder[A, Linear_Set[A]] = new SetBuilder[A, Linear_Set[A]](empty[A])
--- a/src/Pure/General/mercurial.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/mercurial.scala Fri Mar 27 22:06:46 2020 +0100
@@ -44,7 +44,7 @@
def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
{
- def find(root: Path): Option[Repository] =
+ @tailrec def find(root: Path): Option[Repository] =
if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
else if (root.is_root) None
else find(root + Path.parent)
@@ -95,7 +95,7 @@
}
def add(files: List[Path]): Unit =
- hg.command("add", files.map(ssh.bash_path(_)).mkString(" "))
+ hg.command("add", files.map(ssh.bash_path).mkString(" "))
def archive(target: String, rev: String = "", options: String = ""): Unit =
hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
--- a/src/Pure/General/multi_map.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/multi_map.scala Fri Mar 27 22:06:46 2020 +0100
@@ -14,7 +14,7 @@
object Multi_Map extends ImmutableMapFactory[Multi_Map]
{
private val empty_val: Multi_Map[Any, Nothing] = new Multi_Map[Any, Nothing](Map.empty)
- override def empty[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
+ override def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
implicit def canBuildFrom[A, B]: CanBuildFrom[Coll, (A, B), Multi_Map[A, B]] =
new MapCanBuildFrom[A, B]
@@ -63,7 +63,7 @@
override def stringPrefix = "Multi_Map"
- override def empty = Multi_Map.empty
+ override def empty: Multi_Map[A, Nothing] = Multi_Map.empty
override def isEmpty: Boolean = rep.isEmpty
override def keySet: Set[A] = rep.keySet
--- a/src/Pure/General/path.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/path.scala Fri Mar 27 22:06:46 2020 +0100
@@ -73,7 +73,7 @@
val current: Path = new Path(Nil)
val root: Path = new Path(List(Root("")))
def named_root(s: String): Path = new Path(List(root_elem(s)))
- def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem(_)))
+ def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem))
def basic(s: String): Path = new Path(List(basic_elem(s)))
def variable(s: String): Path = new Path(List(variable_elem(s)))
val parent: Path = new Path(List(Parent))
--- a/src/Pure/General/pretty.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/pretty.scala Fri Mar 27 22:06:46 2020 +0100
@@ -6,6 +6,8 @@
package isabelle
+import scala.annotation.tailrec
+
object Pretty
{
@@ -69,7 +71,7 @@
{
val indent1 = force_nat(indent)
- def body_length(prts: List[Tree], len: Double): Double =
+ @tailrec def body_length(prts: List[Tree], len: Double): Double =
{
val (line, rest) =
Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
@@ -104,7 +106,7 @@
private def force_break(tree: Tree): Tree =
tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
- private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
+ private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break)
private def force_next(trees: List[Tree]): List[Tree] =
trees match {
@@ -113,8 +115,8 @@
case t :: ts => t :: force_next(ts)
}
- val default_margin = 76.0
- val default_breakgain = default_margin / 20
+ val default_margin: Double = 76.0
+ val default_breakgain: Double = default_margin / 20
def formatted(input: XML.Body,
margin: Double = default_margin,
--- a/src/Pure/General/properties.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/properties.scala Fri Mar 27 22:06:46 2020 +0100
@@ -67,7 +67,7 @@
XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))
xml_cache match {
case None => ps
- case Some(cache) => ps.map(cache.props(_))
+ case Some(cache) => ps.map(cache.props)
}
}
}
--- a/src/Pure/General/scan.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/scan.scala Fri Mar 27 22:06:46 2020 +0100
@@ -10,10 +10,10 @@
import scala.annotation.tailrec
import scala.collection.{IndexedSeq, Traversable, TraversableOnce}
import scala.collection.immutable.PagedSeq
+import scala.util.matching.Regex
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition,
Reader, CharSequenceReader}
import scala.util.parsing.combinator.RegexParsers
-
import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream}
import java.net.URL
@@ -39,7 +39,7 @@
trait Parsers extends RegexParsers
{
- override val whiteSpace = "".r
+ override val whiteSpace: Regex = "".r
/* optional termination */
@@ -237,7 +237,7 @@
{
require(depth >= 0)
- val comment_text =
+ val comment_text: Parser[List[String]] =
rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r)
def apply(in: Input) =
@@ -399,7 +399,7 @@
else this ++ other.raw_iterator
def -- (remove: Traversable[String]): Lexicon =
- if (remove.exists(contains(_)))
+ if (remove.exists(contains))
Lexicon.empty ++ iterator.filterNot(a => remove.exists(b => a == b))
else this
--- a/src/Pure/General/sql.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/sql.scala Fri Mar 27 22:06:46 2020 +0100
@@ -37,7 +37,7 @@
}
def string(s: String): Source =
- s.iterator.map(escape_char(_)).mkString("'", "", "'")
+ s.iterator.map(escape_char).mkString("'", "", "'")
def ident(s: String): Source =
Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))
@@ -288,7 +288,7 @@
}
def date(column: Column): Date = stmt.db.date(res, column)
- def timing(c1: Column, c2: Column, c3: Column) =
+ def timing(c1: Column, c2: Column, c3: Column): Timing =
Timing(Time.ms(long(c1)), Time.ms(long(c2)), Time.ms(long(c3)))
def get[A](column: Column, f: Column => A): Option[A] =
@@ -296,13 +296,13 @@
val x = f(column)
if (rep.wasNull) None else Some(x)
}
- def get_bool(column: Column): Option[Boolean] = get(column, bool _)
- def get_int(column: Column): Option[Int] = get(column, int _)
- def get_long(column: Column): Option[Long] = get(column, long _)
- def get_double(column: Column): Option[Double] = get(column, double _)
- def get_string(column: Column): Option[String] = get(column, string _)
- def get_bytes(column: Column): Option[Bytes] = get(column, bytes _)
- def get_date(column: Column): Option[Date] = get(column, date _)
+ def get_bool(column: Column): Option[Boolean] = get(column, bool)
+ def get_int(column: Column): Option[Int] = get(column, int)
+ def get_long(column: Column): Option[Long] = get(column, long)
+ def get_double(column: Column): Option[Double] = get(column, double)
+ def get_string(column: Column): Option[String] = get(column, string)
+ def get_bytes(column: Column): Option[Bytes] = get(column, bytes)
+ def get_date(column: Column): Option[Date] = get(column, date)
}
--- a/src/Pure/General/ssh.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/ssh.scala Fri Mar 27 22:06:46 2020 +0100
@@ -10,6 +10,7 @@
import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
import scala.collection.mutable
+import scala.util.matching.Regex
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS}
@@ -21,7 +22,7 @@
object Target
{
- val User_Host = "^([^@]+)@(.+)$".r
+ val User_Host: Regex = "^([^@]+)@(.+)$".r
def parse(s: String): (String, String) =
s match {
@@ -76,7 +77,7 @@
jsch.setKnownHosts(File.platform_path(known_hosts))
val identity_files =
- space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
+ space_explode(':', options.string("ssh_identity_files")).map(Path.explode)
for (identity_file <- identity_files if identity_file.is_file)
jsch.addIdentity(File.platform_path(identity_file))
@@ -431,12 +432,12 @@
def read_file(path: Path, local_path: Path): Unit =
sftp.get(remote_path(path), File.platform_path(local_path))
def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
- def read(path: Path): String = using(open_input(path))(File.read_stream(_))
+ def read(path: Path): String = using(open_input(path))(File.read_stream)
def write_file(path: Path, local_path: Path): Unit =
sftp.put(File.platform_path(local_path), remote_path(path))
def write_bytes(path: Path, bytes: Bytes): Unit =
- using(open_output(path))(bytes.write_stream(_))
+ using(open_output(path))(bytes.write_stream)
def write(path: Path, text: String): Unit =
using(open_output(path))(stream => Bytes(text).write_stream(stream))
--- a/src/Pure/General/symbol.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/symbol.scala Fri Mar 27 22:06:46 2020 +0100
@@ -113,8 +113,8 @@
{
private val matcher = new Matcher(text)
private var i = 0
- def hasNext = i < text.length
- def next =
+ def hasNext: Boolean = i < text.length
+ def next: Symbol =
{
val n = matcher(i, text.length)
val s =
@@ -135,10 +135,10 @@
def length(text: CharSequence): Int = iterator(text).length
def trim_blanks(text: CharSequence): String =
- Library.trim(is_blank(_), explode(text)).mkString
+ Library.trim(is_blank, explode(text)).mkString
def all_blank(str: String): Boolean =
- iterator(str).forall(is_blank(_))
+ iterator(str).forall(is_blank)
def trim_blank_lines(text: String): String =
cat_lines(split_lines(text).dropWhile(all_blank).reverse.dropWhile(all_blank).reverse)
@@ -191,7 +191,7 @@
if (i < 0) sym
else index(i).chr + sym - index(i).sym
}
- def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
+ def decode(symbol_range: Range): Text.Range = symbol_range.map(decode)
override def hashCode: Int = hash
override def equals(that: Any): Boolean =
@@ -448,7 +448,7 @@
/* classification */
- val letters = recode_set(
+ val letters: Set[String] = recode_set(
"A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
"N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
"a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
@@ -481,12 +481,12 @@
"\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
"\\<Psi>", "\\<Omega>")
- val blanks = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n")
+ val blanks: Set[String] = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n")
val sym_chars =
Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
- val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
+ val symbolic: Set[String] = recode_set((for {(sym, _) <- symbols; if raw_symbolic(sym)} yield sym): _*)
/* misc symbols */
--- a/src/Pure/General/url.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/url.scala Fri Mar 27 22:06:46 2020 +0100
@@ -24,7 +24,7 @@
}
else c.toString
- def escape_special(s: String): String = s.iterator.map(escape_special(_)).mkString
+ def escape_special(s: String): String = s.iterator.map(escape_special).mkString
def escape_name(name: String): String =
name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString
--- a/src/Pure/General/value.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/value.scala Fri Mar 27 22:06:46 2020 +0100
@@ -70,7 +70,7 @@
val s = t.seconds
if (s.toInt.toDouble == s) s.toInt.toString else t.toString
}
- def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
+ def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds)
def parse(s: java.lang.String): Time =
unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))
}
--- a/src/Pure/General/word.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/General/word.scala Fri Mar 27 22:06:46 2020 +0100
@@ -53,11 +53,11 @@
}
def unapply(str: String): Option[Case] =
if (str.nonEmpty) {
- if (Codepoint.iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
- else if (Codepoint.iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
+ if (Codepoint.iterator(str).forall(Character.isLowerCase)) Some(Lowercase)
+ else if (Codepoint.iterator(str).forall(Character.isUpperCase)) Some(Uppercase)
else {
val it = Codepoint.iterator(str)
- if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_)))
+ if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase))
Some(Capitalized)
else None
}
--- a/src/Pure/Isar/keyword.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Isar/keyword.scala Fri Mar 27 22:06:46 2020 +0100
@@ -169,7 +169,7 @@
val kinds1 = kinds + (name -> kind)
val load_commands1 =
if (kind == THY_LOAD) {
- if (!Symbol.iterator(name).forall(Symbol.is_ascii(_)))
+ if (!Symbol.iterator(name).forall(Symbol.is_ascii))
error("Bad theory load command " + quote(name))
load_commands + (name -> exts)
}
--- a/src/Pure/Isar/line_structure.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Isar/line_structure.scala Fri Mar 27 22:06:46 2020 +0100
@@ -9,7 +9,7 @@
object Line_Structure
{
- val init = Line_Structure()
+ val init: Line_Structure = Line_Structure()
}
sealed case class Line_Structure(
--- a/src/Pure/Isar/outer_syntax.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Fri Mar 27 22:06:46 2020 +0100
@@ -193,7 +193,7 @@
if (tok.is_ignored) ignored += tok
else if (keywords.is_before_command(tok) ||
tok.is_command &&
- (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
+ (!content.exists(keywords.is_before_command) || content.exists(_.is_command)))
{ flush(); content += tok }
else { content ++= ignored; ignored.clear; content += tok }
}
--- a/src/Pure/Isar/token.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Isar/token.scala Fri Mar 27 22:06:46 2020 +0100
@@ -249,9 +249,9 @@
private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader
{
- def first = tokens.head
- def rest = new Token_Reader(tokens.tail, pos.advance(first))
- def atEnd = tokens.isEmpty
+ def first: Token = tokens.head
+ def rest: Token_Reader = new Token_Reader(tokens.tail, pos.advance(first))
+ def atEnd: Boolean = tokens.isEmpty
}
def reader(tokens: List[Token], start: Token.Pos): Reader =
@@ -321,8 +321,8 @@
source.startsWith(Symbol.open) ||
source.startsWith(Symbol.open_decoded))
- def is_open_bracket: Boolean = is_keyword && Word.open_brackets.exists(is_keyword(_))
- def is_close_bracket: Boolean = is_keyword && Word.close_brackets.exists(is_keyword(_))
+ def is_open_bracket: Boolean = is_keyword && Word.open_brackets.exists(is_keyword)
+ def is_close_bracket: Boolean = is_keyword && Word.close_brackets.exists(is_keyword)
def is_begin: Boolean = is_keyword("begin")
def is_end: Boolean = is_command("end")
@@ -341,7 +341,7 @@
{
val s = content
is_name && Path.is_wellformed(s) &&
- !s.exists(Symbol.is_ascii_blank(_)) &&
+ !s.exists(Symbol.is_ascii_blank) &&
!Path.is_reserved(s)
}
}
--- a/src/Pure/ML/ml_console.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/ML/ml_console.scala Fri Mar 27 22:06:46 2020 +0100
@@ -50,6 +50,9 @@
if (more_args.nonEmpty) getopts.usage()
+ val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+ val store = Sessions.store(options)
+
// build logic
if (!no_build && !raw_ml_system) {
val progress = new Console_Progress()
@@ -62,10 +65,10 @@
// process loop
val process =
- ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
+ ML_Process(options, sessions_structure, store,
+ logic = logic, args = List("-i"), redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
raw_ml_system = raw_ml_system,
- store = Some(Sessions.store(options)),
session_base =
if (raw_ml_system) None
else Some(Sessions.base_info(
--- a/src/Pure/ML/ml_process.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/ML/ml_process.scala Fri Mar 27 22:06:46 2020 +0100
@@ -13,31 +13,26 @@
object ML_Process
{
def apply(options: Options,
+ sessions_structure: Sessions.Structure,
+ store: Sessions.Store,
logic: String = "",
args: List[String] = Nil,
- dirs: List[Path] = Nil,
modes: List[String] = Nil,
raw_ml_system: Boolean = false,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => (),
- sessions_structure: Option[Sessions.Structure] = None,
- session_base: Option[Sessions.Base] = None,
- store: Option[Sessions.Store] = None): Bash.Process =
+ session_base: Option[Sessions.Base] = None): Bash.Process =
{
val logic_name = Isabelle_System.default_logic(logic)
- val _store = store.getOrElse(Sessions.store(options))
-
- val sessions_structure1 =
- sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
val heaps: List[String] =
if (raw_ml_system) Nil
else {
- sessions_structure1.selection(Sessions.Selection.session(logic_name)).
+ sessions_structure.selection(Sessions.Selection.session(logic_name)).
build_requirements(List(logic_name)).
- map(a => File.platform_path(_store.the_heap(a)))
+ map(a => File.platform_path(store.the_heap(a)))
}
val eval_init =
@@ -96,8 +91,8 @@
ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
List("Resources.init_session_base" +
- " {session_positions = " + print_sessions(sessions_structure1.session_positions) +
- ", session_directories = " + print_table(sessions_structure1.dest_session_directories) +
+ " {session_positions = " + print_sessions(sessions_structure.session_positions) +
+ ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
", docs = " + print_list(base.doc_names) +
", global_theories = " + print_table(base.global_theories.toList) +
", loaded_theories = " + print_list(base.loaded_theories.keys) + "}")
@@ -182,8 +177,12 @@
val more_args = getopts(args)
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
- val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
- result().print_stdout.rc
+ val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+ val store = Sessions.store(options)
+
+ val rc =
+ ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes)
+ .result().print_stdout.rc
sys.exit(rc)
})
}
--- a/src/Pure/ML/ml_statistics.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/ML/ml_statistics.scala Fri Mar 27 22:06:46 2020 +0100
@@ -208,7 +208,7 @@
chart(fields._1, fields._2)
def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
- fields.map(chart(_)).foreach(c =>
+ fields.map(chart).foreach(c =>
GUI_Thread.later {
new Frame {
iconImage = GUI.isabelle_image()
--- a/src/Pure/ML/ml_syntax.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/ML/ml_syntax.scala Fri Mar 27 22:06:46 2020 +0100
@@ -37,13 +37,13 @@
private def print_symbol(s: Symbol.Symbol): String =
if (s.startsWith("\\<")) s
- else UTF8.bytes(s).iterator.map(print_byte(_)).mkString
+ else UTF8.bytes(s).iterator.map(print_byte).mkString
def print_string_bytes(str: String): String =
- quote(UTF8.bytes(str).iterator.map(print_byte(_)).mkString)
+ quote(UTF8.bytes(str).iterator.map(print_byte).mkString)
def print_string_symbols(str: String): String =
- quote(Symbol.iterator(str).map(print_symbol(_)).mkString)
+ quote(Symbol.iterator(str).map(print_symbol).mkString)
/* pair */
@@ -61,5 +61,5 @@
/* properties */
def print_properties(props: Properties.T): String =
- print_list(print_pair(print_string_bytes(_), print_string_bytes(_))(_))(props)
+ print_list(print_pair(print_string_bytes, print_string_bytes))(props)
}
--- a/src/Pure/PIDE/document.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/document.scala Fri Mar 27 22:06:46 2020 +0100
@@ -95,12 +95,12 @@
copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
}
- val no_header = Header()
+ val no_header: Header = Header()
def bad_header(msg: String): Header = Header(errors = List(msg))
object Name
{
- val empty = Name("")
+ val empty: Name = Name("")
object Ordering extends scala.math.Ordering[Name]
{
@@ -375,7 +375,7 @@
}
def purge_suppressed: Option[Nodes] =
- graph.keys_iterator.filter(is_suppressed(_)).toList match {
+ graph.keys_iterator.filter(is_suppressed).toList match {
case Nil => None
case del => Some(new Nodes((graph /: del)(_.del_node(_))))
}
@@ -527,7 +527,7 @@
object Snapshot
{
- val init = State.init.snapshot()
+ val init: Snapshot = State.init.snapshot()
}
abstract class Snapshot
@@ -737,13 +737,13 @@
{
execs.get(id) match {
case Some(st) =>
- val new_st = st.accumulate(self_id(st), other_id _, message, xml_cache)
+ val new_st = st.accumulate(self_id(st), other_id, message, xml_cache)
val execs1 = execs + (id -> new_st)
(new_st, copy(execs = execs1, commands_redirection = redirection(new_st)))
case None =>
commands.get(id) match {
case Some(st) =>
- val new_st = st.accumulate(self_id(st), other_id _, message, xml_cache)
+ val new_st = st.accumulate(self_id(st), other_id, message, xml_cache)
val commands1 = commands + (id -> new_st)
(new_st, copy(commands = commands1, commands_redirection = redirection(new_st)))
case None => fail
@@ -1039,11 +1039,11 @@
/* local node content */
- def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
- def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+ def convert(offset: Text.Offset): Text.Offset = (offset /: edits)((i, edit) => edit.convert(i))
+ def revert(offset: Text.Offset): Text.Offset = (offset /: reverse_edits)((i, edit) => edit.revert(i))
- def convert(range: Text.Range) = range.map(convert(_))
- def revert(range: Text.Range) = range.map(revert(_))
+ def convert(range: Text.Range): Text.Range = range.map(convert)
+ def revert(range: Text.Range): Text.Range = range.map(revert)
val node_name: Node.Name = name
val node: Node = version.nodes(name)
@@ -1166,7 +1166,7 @@
case some => Some(some)
}
}
- for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1 _, status))
+ for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
yield Text.Info(r, x)
}
--- a/src/Pure/PIDE/document_id.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/document_id.scala Fri Mar 27 22:06:46 2020 +0100
@@ -17,7 +17,7 @@
type Exec = Generic
val none: Generic = 0
- val make = Counter.make()
+ val make: Counter = Counter.make()
def apply(id: Generic): String = Value.Long.apply(id)
def unapply(s: String): Option[Generic] = Value.Long.unapply(s)
--- a/src/Pure/PIDE/document_status.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/document_status.scala Fri Mar 27 22:06:46 2020 +0100
@@ -55,7 +55,7 @@
runs = runs)
}
- val empty = make(Iterator.empty)
+ val empty: Command_Status = make(Iterator.empty)
def merge(status_iterator: Iterator[Command_Status]): Command_Status =
if (status_iterator.hasNext) {
--- a/src/Pure/PIDE/headless.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/headless.scala Fri Mar 27 22:06:46 2020 +0100
@@ -224,7 +224,7 @@
}
else result
- val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory(_))
+ val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory)
(load_theories,
copy(already_committed = already_committed1, result = result1, load_state = load_state1))
@@ -350,7 +350,7 @@
(theory_progress, st.update(nodes_status1))
})
- theory_progress.foreach(progress.theory(_))
+ theory_progress.foreach(progress.theory)
check_state()
@@ -396,8 +396,8 @@
object Resources
{
- def apply(base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
- new Resources(base_info, log = log)
+ def apply(options: Options, base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
+ new Resources(options, base_info, log = log)
def make(
options: Options,
@@ -410,7 +410,7 @@
val base_info =
Sessions.base_info(options, session_name, dirs = session_dirs,
include_sessions = include_sessions, progress = progress)
- apply(base_info, log = log)
+ apply(options, base_info, log = log)
}
final class Theory private[Headless](
@@ -496,7 +496,7 @@
lazy val theory_graph: Document.Node.Name.Graph[Unit] =
Document.Node.Name.make_graph(
for ((name, theory) <- theories.toList)
- yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_))))
+ yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt)))
def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
@@ -542,7 +542,7 @@
: ((List[Document.Node.Name], List[Document.Node.Name], List[Document.Edit_Text]), State) =
{
val all_nodes = theory_graph.topological_order
- val purge = nodes.getOrElse(all_nodes).filterNot(is_required(_)).toSet
+ val purge = nodes.getOrElse(all_nodes).filterNot(is_required).toSet
val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
val (retained, purged) = all_nodes.partition(retain)
@@ -554,6 +554,7 @@
}
class Resources private[Headless](
+ val options: Options,
val session_base_info: Sessions.Base_Info,
log: Logger = No_Logger)
extends isabelle.Resources(
@@ -561,7 +562,7 @@
{
resources =>
- def options: Options = session_base_info.options
+ val store: Sessions.Store = Sessions.store(options)
/* session */
@@ -585,8 +586,8 @@
session.phase_changed += session_phase
progress.echo("Starting session " + session_base_info.session + " ...")
- Isabelle_Process.start(session, options,
- logic = session_base_info.session, dirs = session_base_info.dirs, modes = print_mode)
+ Isabelle_Process(session, options, session_base_info.sessions_structure, store,
+ logic = session_base_info.session, modes = print_mode)
session_error.join match {
case "" => session
--- a/src/Pure/PIDE/markup.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/markup.scala Fri Mar 27 22:06:46 2020 +0100
@@ -58,8 +58,8 @@
/* basic markup */
- val Empty = Markup("", Nil)
- val Broken = Markup("broken", Nil)
+ val Empty: Markup = Markup("", Nil)
+ val Broken: Markup = Markup("broken", Nil)
class Markup_String(val name: String, prop: String)
{
--- a/src/Pure/PIDE/protocol.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala Fri Mar 27 22:06:46 2020 +0100
@@ -32,7 +32,7 @@
case a :: bs => (a, bs)
case _ => throw new XML.XML_Body(body)
}
- Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text)))
+ Some(triple(long, list(string), list(decode_upd))(Symbol.decode_yxml(text)))
}
catch {
case ERROR(_) => None
@@ -310,7 +310,7 @@
def define_commands_bulk(commands: List[Command])
{
val (irregular, regular) = commands.partition(command => YXML.detect(command.source))
- irregular.foreach(define_command(_))
+ irregular.foreach(define_command)
regular match {
case Nil =>
case List(command) => define_command(command)
--- a/src/Pure/PIDE/prover.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/prover.scala Fri Mar 27 22:06:46 2020 +0100
@@ -32,14 +32,14 @@
def properties: Properties.T = message.markup.properties
def body: XML.Body = message.body
- def is_init = kind == Markup.INIT
- def is_exit = kind == Markup.EXIT
- def is_stdout = kind == Markup.STDOUT
- def is_stderr = kind == Markup.STDERR
- def is_system = kind == Markup.SYSTEM
- def is_status = kind == Markup.STATUS
- def is_report = kind == Markup.REPORT
- def is_syslog = is_init || is_exit || is_system || is_stderr
+ def is_init: Boolean = kind == Markup.INIT
+ def is_exit: Boolean = kind == Markup.EXIT
+ def is_stdout: Boolean = kind == Markup.STDOUT
+ def is_stderr: Boolean = kind == Markup.STDERR
+ def is_system: Boolean = kind == Markup.SYSTEM
+ def is_status: Boolean = kind == Markup.STATUS
+ def is_report: Boolean = kind == Markup.REPORT
+ def is_syslog: Boolean = is_init || is_exit || is_system || is_stderr
override def toString: String =
{
--- a/src/Pure/PIDE/rendering.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala Fri Mar 27 22:06:46 2020 +0100
@@ -21,20 +21,20 @@
// background
val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result,
markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value
- val background_colors = values
+ val background_colors: ValueSet = values
// foreground
val quoted, antiquoted = Value
- val foreground_colors = values -- background_colors
+ val foreground_colors: ValueSet = values -- background_colors
// message underline
val writeln, information, warning, legacy, error = Value
- val message_underline_colors = values -- background_colors -- foreground_colors
+ val message_underline_colors: ValueSet = values -- background_colors -- foreground_colors
// message background
val writeln_message, information_message, tracing_message,
warning_message, legacy_message, error_message = Value
- val message_background_colors =
+ val message_background_colors: ValueSet =
values -- background_colors -- foreground_colors -- message_underline_colors
// text
@@ -42,7 +42,7 @@
tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted,
inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter,
antiquote, raw_text, plain_text = Value
- val text_colors =
+ val text_colors: ValueSet =
values -- background_colors -- foreground_colors -- message_underline_colors --
message_background_colors
--- a/src/Pure/PIDE/session.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/session.scala Fri Mar 27 22:06:46 2020 +0100
@@ -213,7 +213,7 @@
private val _phase = Synchronized[Session.Phase](Session.Inactive)
private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase))
- def phase = _phase.value
+ def phase: Session.Phase = _phase.value
def is_ready: Boolean = phase == Session.Ready
@@ -645,7 +645,7 @@
case Session.Change_Flush if prover.defined =>
val state = global_state.value
if (!state.removing_versions)
- postponed_changes.flush(state).foreach(handle_change(_))
+ postponed_changes.flush(state).foreach(handle_change)
case bad =>
if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
--- a/src/Pure/PIDE/xml.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/xml.scala Fri Mar 27 22:06:46 2020 +0100
@@ -217,7 +217,7 @@
else
lookup(x) match {
case Some(y) => y
- case None => x.map(cache_tree(_))
+ case None => x.map(cache_tree)
}
}
--- a/src/Pure/PIDE/yxml.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/PIDE/yxml.scala Fri Mar 27 22:06:46 2020 +0100
@@ -21,10 +21,10 @@
val is_X = (c: Char) => c == X
val is_Y = (c: Char) => c == Y
- val X_string = X.toString
- val Y_string = Y.toString
- val XY_string = X_string + Y_string
- val XYX_string = XY_string + X_string
+ val X_string: String = X.toString
+ val Y_string: String = Y.toString
+ val XY_string: String = X_string + Y_string
+ val XYX_string: String = XY_string + X_string
def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
def detect_elem(s: String): Boolean = s.startsWith(XY_string)
--- a/src/Pure/System/bash.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/System/bash.scala Fri Mar 27 22:06:46 2020 +0100
@@ -35,10 +35,10 @@
def string(s: String): String =
if (s == "") "\"\""
- else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
+ else UTF8.bytes(s).iterator.map(bash_chr).mkString
def strings(ss: List[String]): String =
- ss.iterator.map(Bash.string(_)).mkString(" ")
+ ss.iterator.map(Bash.string).mkString(" ")
/* process and result */
--- a/src/Pure/System/getopts.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/System/getopts.scala Fri Mar 27 22:06:46 2020 +0100
@@ -7,6 +7,9 @@
package isabelle
+import scala.annotation.tailrec
+
+
object Getopts
{
def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
@@ -44,7 +47,7 @@
cat_error(msg, "The error(s) above occurred in command-line option " + print_option(opt))
}
- private def getopts(args: List[List[Char]]): List[List[Char]] =
+ @tailrec private def getopts(args: List[List[Char]]): List[List[Char]] =
args match {
case List('-', '-') :: rest_args => rest_args
case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && rest_opts.nonEmpty =>
--- a/src/Pure/System/invoke_scala.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/System/invoke_scala.scala Fri Mar 27 22:06:46 2020 +0100
@@ -123,6 +123,6 @@
val functions =
List(
- Markup.INVOKE_SCALA -> invoke_scala _,
- Markup.CANCEL_SCALA -> cancel_scala _)
+ Markup.INVOKE_SCALA -> invoke_scala,
+ Markup.CANCEL_SCALA -> cancel_scala)
}
--- a/src/Pure/System/isabelle_process.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/System/isabelle_process.scala Fri Mar 27 22:06:46 2020 +0100
@@ -12,52 +12,33 @@
object Isabelle_Process
{
- def start(session: Session,
+ def apply(
+ session: Session,
options: Options,
+ sessions_structure: Sessions.Structure,
+ store: Sessions.Store,
logic: String = "",
args: List[String] = Nil,
- dirs: List[Path] = Nil,
modes: List[String] = Nil,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
- sessions_structure: Option[Sessions.Structure] = None,
- store: Option[Sessions.Store] = None,
phase_changed: Session.Phase => Unit = null)
{
- if (phase_changed != null)
- session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
-
- session.start(receiver =>
- Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
- cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache,
- sessions_structure = sessions_structure, store = store))
- }
-
- def apply(
- options: Options,
- logic: String = "",
- args: List[String] = Nil,
- dirs: List[Path] = Nil,
- modes: List[String] = Nil,
- cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings(),
- receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
- xml_cache: XML.Cache = XML.make_cache(),
- sessions_structure: Option[Sessions.Structure] = None,
- store: Option[Sessions.Store] = None): Prover =
- {
val channel = System_Channel()
val process =
try {
val channel_options =
options.string.update("system_channel_address", channel.address).
string.update("system_channel_password", channel.password)
- ML_Process(channel_options, logic = logic, args = args, dirs = dirs, modes = modes,
- cwd = cwd, env = env, sessions_structure = sessions_structure, store = store)
+ ML_Process(channel_options, sessions_structure, store,
+ logic = logic, args = args, modes = modes, cwd = cwd, env = env)
}
catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
process.stdin.close
- new Prover(receiver, xml_cache, channel, process)
+ if (phase_changed != null)
+ session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
+
+ session.start(receiver => new Prover(receiver, session.xml_cache, channel, process))
}
}
--- a/src/Pure/System/numa.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/System/numa.scala Fri Mar 27 22:06:46 2020 +0100
@@ -26,7 +26,7 @@
}
if (numa_nodes_linux.is_file) {
- space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
+ space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read)
}
else Nil
}
--- a/src/Pure/System/options.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/System/options.scala Fri Mar 27 22:06:46 2020 +0100
@@ -55,7 +55,7 @@
case word :: rest if word == strip => rest
case _ => words
}
- Word.implode(words1.map(Word.perhaps_capitalize(_)))
+ Word.implode(words1.map(Word.perhaps_capitalize))
}
def unknown: Boolean = typ == Unknown
@@ -70,19 +70,19 @@
private val OPTIONS = Path.explode("etc/options")
private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
- val options_syntax =
+ val options_syntax: Outer_Syntax =
Outer_Syntax.empty + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
(SECTION, Keyword.DOCUMENT_HEADING) +
(PUBLIC, Keyword.BEFORE_COMMAND) +
(OPTION, Keyword.THY_DECL)
- val prefs_syntax = Outer_Syntax.empty + "="
+ val prefs_syntax: Outer_Syntax = Outer_Syntax.empty + "="
trait Parser extends Parse.Parser
{
- val option_name = atom("option name", _.is_name)
- val option_type = atom("option type", _.is_name)
- val option_value =
+ val option_name: Parser[String] = atom("option name", _.is_name)
+ val option_type: Parser[String] = atom("option type", _.is_name)
+ val option_value: Parser[String] =
opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
{ case s ~ n => if (s.isDefined) "-" + n else n } |
atom("option value", tok => tok.is_name || tok.is_float)
--- a/src/Pure/System/progress.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/System/progress.scala Fri Mar 27 22:06:46 2020 +0100
@@ -34,7 +34,7 @@
def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
- Timing.timeit(message, enabled, echo(_))(e)
+ Timing.timeit(message, enabled, echo)(e)
def stopped: Boolean = false
def interrupt_handler[A](e: => A): A = e
--- a/src/Pure/Thy/export.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Thy/export.scala Fri Mar 27 22:06:46 2020 +0100
@@ -312,7 +312,7 @@
// list
if (export_list) {
(for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
- sorted.foreach(progress.echo(_))
+ sorted.foreach(progress.echo)
}
// export
@@ -348,7 +348,7 @@
/* Isabelle tool wrapper */
- val default_export_dir = Path.explode("export")
+ val default_export_dir: Path = Path.explode("export")
val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
{
--- a/src/Pure/Thy/export_theory.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Thy/export_theory.scala Fri Mar 27 22:06:46 2020 +0100
@@ -23,7 +23,7 @@
else None
def theories: List[Theory] =
- theory_graph.topological_order.flatMap(theory(_))
+ theory_graph.topological_order.flatMap(theory)
}
def read_session(
--- a/src/Pure/Thy/file_format.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Thy/file_format.scala Fri Mar 27 22:06:46 2020 +0100
@@ -56,7 +56,7 @@
trait File_Format
{
def format_name: String
- override def toString = format_name
+ override def toString: String = format_name
def file_ext: String
def detect(name: String): Boolean = name.endsWith("." + file_ext)
--- a/src/Pure/Thy/html.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Thy/html.scala Fri Mar 27 22:06:46 2020 +0100
@@ -368,7 +368,7 @@
(if (entry.is_italic) List(" font-style: italic;") else Nil) :::
List("}"))
- ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face(_)))
+ ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face))
.mkString("", "\n\n", "\n")
}
--- a/src/Pure/Thy/latex.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Thy/latex.scala Fri Mar 27 22:06:46 2020 +0100
@@ -10,6 +10,7 @@
import java.io.{File => JFile}
import scala.annotation.tailrec
+import scala.util.matching.Regex
object Latex
@@ -102,7 +103,7 @@
object File_Line_Error
{
- val Pattern = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
+ val Pattern: Regex = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
def unapply(line: String): Option[(Path, Int, String)] =
line match {
case Pattern(file, Value.Int(line), message) =>
--- a/src/Pure/Thy/sessions.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Mar 27 22:06:46 2020 +0100
@@ -235,7 +235,7 @@
(Graph_Display.empty_graph /: required_subgraph.topological_order)(
{ case (g, session) =>
val a = session_node(session)
- val bs = required_subgraph.imm_preds(session).toList.map(session_node(_))
+ val bs = required_subgraph.imm_preds(session).toList.map(session_node)
((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
(graph0 /: dependencies.entries)(
@@ -271,7 +271,7 @@
if !ok(path.canonical_file)
path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
} yield (path1, name)).toList
- val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).toSet.toList.sorted
+ val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted
val errs1 =
for { (path1, name) <- bad }
@@ -336,8 +336,6 @@
/* base info */
sealed case class Base_Info(
- options: Options,
- dirs: List[Path],
session: String,
sessions_structure: Structure,
errors: List[String],
@@ -371,7 +369,7 @@
deps.get(ancestor.get) match {
case Some(ancestor_base)
if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) =>
- ancestor_base.loaded_theories.defined(_)
+ ancestor_base.loaded_theories.defined _
case _ =>
error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
}
@@ -420,7 +418,7 @@
val deps1 = Sessions.deps(selected_sessions1, progress = progress)
- Base_Info(options, dirs, session1, full_sessions1, deps1.errors, deps1(session1), infos1)
+ Base_Info(session1, full_sessions1, deps1.errors, deps1(session1), infos1)
}
@@ -654,7 +652,7 @@
def check_sessions(names: List[String])
{
- val bad_sessions = SortedSet(names.filterNot(defined(_)): _*).toList
+ val bad_sessions = SortedSet(names.filterNot(defined): _*).toList
if (bad_sessions.nonEmpty)
error("Undefined session(s): " + commas_quote(bad_sessions))
}
@@ -746,8 +744,8 @@
/* parser */
- val ROOT = Path.explode("ROOT")
- val ROOTS = Path.explode("ROOTS")
+ val ROOT: Path = Path.explode("ROOT")
+ val ROOTS: Path = Path.explode("ROOTS")
private val CHAPTER = "chapter"
private val SESSION = "session"
@@ -761,7 +759,7 @@
private val DOCUMENT_FILES = "document_files"
private val EXPORT_FILES = "export_files"
- val root_syntax =
+ val root_syntax: Outer_Syntax =
Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
GLOBAL + IN +
(CHAPTER, Keyword.THY_DECL) +
@@ -897,7 +895,7 @@
def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
{
- val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
+ val default_dirs = Isabelle_System.components().filter(is_session_dir)
for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }
yield (select, dir.canonical)
}
@@ -1075,7 +1073,7 @@
input_dirs.map(_ + heap(name)).find(_.is_file)
def find_heap_digest(name: String): Option[String] =
- find_heap(name).flatMap(read_heap_digest(_))
+ find_heap(name).flatMap(read_heap_digest)
def the_heap(name: String): Path =
find_heap(name) getOrElse
@@ -1107,7 +1105,7 @@
if (output || has_session_info(db, name)) Some(db) else { db.close; None }
}
else if (output) Some(SQLite.open_database(output_database(name)))
- else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database(_))
+ else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database)
}
def open_database(name: String, output: Boolean = false): SQL.Database =
--- a/src/Pure/Thy/thy_syntax.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Fri Mar 27 22:06:46 2020 +0100
@@ -136,7 +136,7 @@
val new_commands = insert_text(Some(cmd), text) - cmd
edit_text(rest.toList ::: es, new_commands)
- case Some((cmd, cmd_start)) =>
+ case Some((cmd, _)) =>
edit_text(es, insert_text(Some(cmd), e.text))
case None =>
--- a/src/Pure/Tools/build.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/build.scala Fri Mar 27 22:06:46 2020 +0100
@@ -250,8 +250,8 @@
val session_result = Future.promise[Process_Result]
- Isabelle_Process.start(session, options, logic = parent, cwd = info.dir.file, env = env,
- sessions_structure = Some(sessions_structure), store = Some(store),
+ Isabelle_Process(session, options, sessions_structure, store,
+ logic = parent, cwd = info.dir.file, env = env,
phase_changed =
{
case Session.Ready => session.protocol_command("build_session", args_yxml)
@@ -280,17 +280,16 @@
val process =
if (Sessions.is_pure(name)) {
- ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
+ ML_Process(options, deps.sessions_structure, store, raw_ml_system = true,
args =
(for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
- List("--eval", eval),
- env = env, sessions_structure = Some(deps.sessions_structure), store = Some(store),
- cleanup = () => args_file.delete)
+ List("--eval", eval),
+ cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
}
else {
- ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
- env = env, sessions_structure = Some(deps.sessions_structure), store = Some(store),
- cleanup = () => args_file.delete)
+ ML_Process(options, deps.sessions_structure, store, logic = parent,
+ args = List("--eval", eval),
+ cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
}
process.result(
@@ -337,7 +336,7 @@
{
val result0 = future_result.join
val result1 =
- export_consumer.shutdown(close = true).map(Output.error_message_text(_)) match {
+ export_consumer.shutdown(close = true).map(Output.error_message_text) match {
case Nil => result0
case errs => result0.errors(errs).error_rc
}
@@ -381,7 +380,7 @@
def cancelled(name: String): Boolean = results(name)._1.isEmpty
def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
def info(name: String): Sessions.Info = results(name)._2
- val rc =
+ val rc: Int =
(0 /: results.iterator.map(
{ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
def ok: Boolean = rc == 0
@@ -581,7 +580,7 @@
}
// messages
- process_result.err_lines.foreach(progress.echo(_))
+ process_result.err_lines.foreach(progress.echo)
if (process_result.ok)
progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
@@ -595,7 +594,7 @@
//}}}
case None if running.size < (max_jobs max 1) =>
//{{{ check/start next job
- pending.dequeue(running.isDefinedAt(_)) match {
+ pending.dequeue(running.isDefinedAt) match {
case Some((name, info)) =>
val ancestor_results =
deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name).
@@ -640,7 +639,7 @@
store.clean_output(name)
using(store.open_database(name, output = true))(store.init_session_info(_, name))
- val numa_node = numa_nodes.next(used_node(_))
+ val numa_node = numa_nodes.next(used_node)
val job =
new Job(progress, name, info, deps, store, do_output, verbose, pide = pide,
numa_node, queue.command_timings(name))
--- a/src/Pure/Tools/debugger.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/debugger.scala Fri Mar 27 22:06:46 2020 +0100
@@ -23,7 +23,7 @@
{
def size: Int = debug_states.length + 1
def reset: Context = copy(index = 0)
- def select(i: Int) = copy(index = i + 1)
+ def select(i: Int): Context = copy(index = i + 1)
def thread_state: Option[Debug_State] = debug_states.headOption
@@ -143,8 +143,8 @@
val functions =
List(
- Markup.DEBUGGER_STATE -> debugger_state _,
- Markup.DEBUGGER_OUTPUT -> debugger_output _)
+ Markup.DEBUGGER_STATE -> debugger_state,
+ Markup.DEBUGGER_OUTPUT -> debugger_output)
}
}
--- a/src/Pure/Tools/doc.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/doc.scala Fri Mar 27 22:06:46 2020 +0100
@@ -46,7 +46,7 @@
private def release_notes(): List[Entry] =
Section("Release Notes", true) ::
- Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_))
+ Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file)
private def examples(): List[Entry] =
Section("Examples", true) ::
--- a/src/Pure/Tools/dump.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/dump.scala Fri Mar 27 22:06:46 2020 +0100
@@ -363,7 +363,7 @@
session.use_theories(used_theories.map(_.theory),
unicode_symbols = unicode_symbols,
progress = progress,
- commit = Some(Consumer.apply _))
+ commit = Some(Consumer.apply))
val bad_theories = Consumer.shutdown()
val bad_msgs =
@@ -463,7 +463,7 @@
Dump cumulative PIDE session database, with the following aspects:
""" + Library.prefix_lines(" ", show_aspects) + "\n",
- "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
+ "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)),
--- a/src/Pure/Tools/fontforge.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/fontforge.scala Fri Mar 27 22:06:46 2020 +0100
@@ -38,7 +38,7 @@
}
if (s.nonEmpty && s(0) == '\\') err('\\')
- s.iterator.map(escape(_)).mkString(q.toString, "", q.toString)
+ s.iterator.map(escape).mkString(q.toString, "", q.toString)
}
def file_name(path: Path): Script = string(File.standard_path(path))
@@ -121,7 +121,7 @@
}
def set: Script =
- List(fontname, familyname, fullname, weight, copyright, fontversion).map(string(_)).
+ List(fontname, familyname, fullname, weight, copyright, fontversion).map(string).
mkString("SetFontNames(", ",", ")")
}
--- a/src/Pure/Tools/phabricator.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/phabricator.scala Fri Mar 27 22:06:46 2020 +0100
@@ -39,7 +39,7 @@
val daemon_user = "phabricator"
- val sshd_config = Path.explode("/etc/ssh/sshd_config")
+ val sshd_config: Path = Path.explode("/etc/ssh/sshd_config")
/* installation parameters */
@@ -59,7 +59,7 @@
val default_mailers: Path = Path.explode("mailers.json")
- val default_system_port = SSH.default_port
+ val default_system_port: Int = SSH.default_port
val alternative_system_port = 222
val default_server_port = 2222
@@ -69,7 +69,7 @@
/** global configuration **/
- val global_config = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
+ val global_config: Path = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
def global_config_script(
init: String = "",
--- a/src/Pure/Tools/print_operation.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/print_operation.scala Fri Mar 27 22:06:46 2020 +0100
@@ -38,6 +38,6 @@
true
}
- val functions = List(Markup.PRINT_OPERATIONS -> put _)
+ val functions = List(Markup.PRINT_OPERATIONS -> put)
}
}
--- a/src/Pure/Tools/server.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/server.scala Fri Mar 27 22:06:46 2020 +0100
@@ -35,8 +35,8 @@
def split(msg: String): (String, String) =
{
- val name = msg.takeWhile(is_name_char(_))
- val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
+ val name = msg.takeWhile(is_name_char)
+ val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank)
(name, argument)
}
@@ -607,7 +607,7 @@
Exn.capture(server_socket.accept) match {
case Exn.Res(socket) =>
Standard_Thread.fork("server_connection")
- { using(Server.Connection(socket))(handle(_)) }
+ { using(Server.Connection(socket))(handle) }
case Exn.Exn(_) => finished = true
}
}
--- a/src/Pure/Tools/server_commands.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/server_commands.scala Fri Mar 27 22:06:46 2020 +0100
@@ -46,10 +46,10 @@
}
def command(args: Args, progress: Progress = No_Progress)
- : (JSON.Object.T, Build.Results, Sessions.Base_Info) =
+ : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) =
{
val options = Options.init(prefs = args.preferences, opts = args.options)
- val dirs = args.dirs.map(Path.explode(_))
+ val dirs = args.dirs.map(Path.explode)
val base_info =
Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
@@ -85,7 +85,7 @@
"timing" -> result.timing.json)
}))
- if (results.ok) (results_json, results, base_info)
+ if (results.ok) (results_json, results, options, base_info)
else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
}
}
@@ -106,11 +106,11 @@
def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
: (JSON.Object.T, (UUID.T, Headless.Session)) =
{
- val base_info =
- try { Session_Build.command(args.build, progress = progress)._3 }
+ val (_, _, options, base_info) =
+ try { Session_Build.command(args.build, progress = progress) }
catch { case exn: Server.Error => error(exn.message) }
- val resources = Headless.Resources(base_info, log = log)
+ val resources = Headless.Resources(options, base_info, log = log)
val session = resources.start_session(print_mode = args.print_mode, progress = progress)
--- a/src/Pure/Tools/spell_checker.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/spell_checker.scala Fri Mar 27 22:06:46 2020 +0100
@@ -66,8 +66,8 @@
class Dictionary private[Spell_Checker](val path: Path)
{
- val lang = path.drop_ext.file_name
- val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
+ val lang: String = path.drop_ext.file_name
+ val user_path: Path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
override def toString: String = lang
}
--- a/src/Pure/Tools/update_cartouches.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/Tools/update_cartouches.scala Fri Mar 27 22:06:46 2020 +0100
@@ -7,13 +7,16 @@
package isabelle
+import scala.util.matching.Regex
+
+
object Update_Cartouches
{
/* update cartouches */
private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
- val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r
+ val Text_Antiq: Regex = """(?s)@\{\s*text\b\s*(.+)\}""".r
def update_text(content: String): String =
{
--- a/src/Pure/library.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/library.scala Fri Mar 27 22:06:46 2020 +0100
@@ -140,7 +140,7 @@
else s
def trim_split_lines(s: String): List[String] =
- split_lines(trim_line(s)).map(trim_line(_))
+ split_lines(trim_line(s)).map(trim_line)
def isolate_substring(s: String): String = new String(s.toCharArray)
@@ -204,7 +204,7 @@
def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
def escape_regex(s: String): String =
- if (s.exists(is_regex_meta(_))) {
+ if (s.exists(is_regex_meta)) {
(for (c <- s.iterator)
yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
}
--- a/src/Pure/term.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Pure/term.scala Fri Mar 27 22:06:46 2020 +0100
@@ -50,7 +50,7 @@
override def toString: String =
"TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
}
- val dummyT = Type("dummy")
+ val dummyT: Type = Type("dummy")
sealed abstract class Term
{
@@ -143,7 +143,7 @@
lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
protected def cache_sort(x: Sort): Sort =
- if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string(_)))
+ if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string))
protected def cache_typ(x: Typ): Typ =
{
@@ -166,7 +166,7 @@
else {
lookup(x) match {
case Some(y) => y
- case None => store(x.map(cache_typ(_)))
+ case None => store(x.map(cache_typ))
}
}
}
--- a/src/Tools/Graphview/graph_file.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/Graphview/graph_file.scala Fri Mar 27 22:06:46 2020 +0100
@@ -30,8 +30,8 @@
}
val name = file.getName
- if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h)
- else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h)
+ if (name.endsWith(".png")) Graphics_File.write_png(file, paint, w, h)
+ else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint, w, h)
else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
}
--- a/src/Tools/Graphview/graphview.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/Graphview/graphview.scala Fri Mar 27 22:06:46 2020 +0100
@@ -82,7 +82,7 @@
}
else node.toString
- _layout = Layout.make(options, metrics, node_text _, visible_graph)
+ _layout = Layout.make(options, metrics, node_text, visible_graph)
}
--- a/src/Tools/Graphview/layout.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/Graphview/layout.scala Fri Mar 27 22:06:46 2020 +0100
@@ -104,7 +104,7 @@
val lines = split_lines(node_text(a, content))
val w2 = metrics.node_width2(lines)
val h2 = metrics.node_height2(lines.length)
- ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node(_)))
+ ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node))
}).toList)
val initial_levels: Levels =
--- a/src/Tools/Graphview/model.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/Graphview/model.scala Fri Mar 27 22:06:46 2020 +0100
@@ -18,7 +18,7 @@
val events = new Mutator_Event.Bus
private var _mutators : List[Mutator.Info] = Nil
- def apply() = _mutators
+ def apply(): List[Mutator.Info] = _mutators
def apply(mutators: List[Mutator.Info])
{
_mutators = mutators
--- a/src/Tools/Graphview/mutator.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/Graphview/mutator.scala Fri Mar 27 22:06:46 2020 +0100
@@ -173,6 +173,6 @@
trait Filter extends Mutator
{
- def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph) = filter(graph)
+ def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph = filter(graph)
def filter(graph: Graph_Display.Graph): Graph_Display.Graph
}
--- a/src/Tools/Graphview/mutator_dialog.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala Fri Mar 27 22:06:46 2020 +0100
@@ -110,7 +110,7 @@
filter_panel.repaint
}
- val filter_panel = new BoxPanel(Orientation.Vertical) {}
+ val filter_panel: BoxPanel = new BoxPanel(Orientation.Vertical) {}
private val mutator_box = new ComboBox[Mutator](container.available)
--- a/src/Tools/VSCode/src/grammar.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/VSCode/src/grammar.scala Fri Mar 27 22:06:46 2020 +0100
@@ -23,7 +23,7 @@
def generate(keywords: Keyword.Keywords): JSON.S =
{
val (minor_keywords, operators) =
- keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier(_))
+ keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier)
def major_keywords(pred: String => Boolean): List[String] =
(for {
@@ -39,7 +39,7 @@
def grouped_names(as: List[String]): String =
- JSON.Format("\\b(" + as.sorted.map(Library.escape_regex(_)).mkString("|") + ")\\b")
+ JSON.Format("\\b(" + as.sorted.map(Library.escape_regex).mkString("|") + ")\\b")
"""{
"name": "Isabelle",
--- a/src/Tools/VSCode/src/server.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/VSCode/src/server.scala Fri Mar 27 22:06:46 2020 +0100
@@ -140,7 +140,7 @@
}
private val file_watcher =
- File_Watcher(sync_documents(_), options.seconds("vscode_load_delay"))
+ File_Watcher(sync_documents, options.seconds("vscode_load_delay"))
private def close_document(file: JFile)
{
@@ -318,8 +318,9 @@
}
session.phase_changed += session_phase
- Isabelle_Process.start(session, options, modes = modes,
- sessions_structure = Some(base_info.sessions_structure), logic = base_info.session)
+ val store = Sessions.store(options)
+ Isabelle_Process(session, options, base_info.sessions_structure, store,
+ modes = modes, logic = base_info.session)
}
}
@@ -485,7 +486,7 @@
channel.read() match {
case Some(json) =>
json match {
- case bulk: List[_] => bulk.foreach(handle(_))
+ case bulk: List[_] => bulk.foreach(handle)
case _ => handle(json)
}
loop()
--- a/src/Tools/jEdit/src/completion_popup.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Mar 27 22:06:46 2020 +0100
@@ -10,7 +10,7 @@
import isabelle._
import java.awt.{Color, Font, Point, BorderLayout, Dimension}
-import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
+import java.awt.event.{KeyEvent, KeyListener, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
import java.io.{File => JFile}
import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
import javax.swing.border.LineBorder
@@ -18,7 +18,6 @@
import scala.swing.{ListView, ScrollPane}
import scala.swing.event.MouseClicked
-
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection}
import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
@@ -399,7 +398,7 @@
/* activation */
private val outer_key_listener =
- JEdit_Lib.key_listener(key_typed = input _)
+ JEdit_Lib.key_listener(key_typed = input)
private def activate()
{
@@ -570,7 +569,7 @@
GUI_Thread.require {}
require(items.nonEmpty)
- val multi = items.length > 1
+ val multi: Boolean = items.length > 1
/* actions */
@@ -621,7 +620,7 @@
/* event handling */
- val inner_key_listener =
+ val inner_key_listener: KeyListener =
JEdit_Lib.key_listener(
key_pressed = (e: KeyEvent) =>
{
@@ -655,7 +654,7 @@
}
propagate(e)
},
- key_typed = propagate _
+ key_typed = propagate
)
list_view.peer.addKeyListener(inner_key_listener)
--- a/src/Tools/jEdit/src/debugger_dockable.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Fri Mar 27 22:06:46 2020 +0100
@@ -74,7 +74,7 @@
val pretty_text_area = new Pretty_Text_Area(view)
- override def detach_operation = pretty_text_area.detach_operation
+ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
private def handle_resize()
{
@@ -208,22 +208,22 @@
private val continue_button = new Button("Continue") {
tooltip = "Continue program on current thread, until next breakpoint"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.continue(_)) }
+ reactions += { case ButtonClicked(_) => thread_selection().map(debugger.continue) }
}
private val step_button = new Button("Step") {
tooltip = "Single-step in depth-first order"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step(_)) }
+ reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step) }
}
private val step_over_button = new Button("Step over") {
tooltip = "Single-step within this function"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_over(_)) }
+ reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_over) }
}
private val step_out_button = new Button("Step out") {
tooltip = "Single-step outside this function"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_out(_)) }
+ reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_out) }
}
private val context_label = new Label("Context:") {
@@ -318,7 +318,7 @@
/* main panel */
- val main_panel = new SplitPane(Orientation.Vertical) {
+ val main_panel: SplitPane = new SplitPane(Orientation.Vertical) {
oneTouchExpandable = true
leftComponent = tree_pane
rightComponent = Component.wrap(pretty_text_area)
--- a/src/Tools/jEdit/src/document_model.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Mar 27 22:06:46 2020 +0100
@@ -81,7 +81,7 @@
private val state = Synchronized(State()) // owned by GUI thread
def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
- def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name)
+ def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
def document_blobs(): Document.Blobs = state.value.document_blobs
@@ -313,7 +313,7 @@
val preview =
HTTP.get(preview_root, arg =>
for {
- query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_))
+ query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
name = Library.perhaps_unprefix(plain_text_prefix, query)
model <- get(PIDE.resources.node_name(name))
}
@@ -348,7 +348,7 @@
if (hidden) Text.Perspective.empty
else {
val view_ranges = document_view_ranges(snapshot)
- val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_))
+ val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node)
Text.Perspective(view_ranges ::: load_ranges)
}
val overlays = PIDE.editor.node_overlays(node_name)
@@ -589,7 +589,7 @@
if (reparse || edits.nonEmpty || last_perspective != perspective) {
pending.clear
last_perspective = perspective
- node_edits(node_header, edits, perspective)
+ node_edits(node_header(), edits, perspective)
}
else Nil
}
--- a/src/Tools/jEdit/src/document_view.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Fri Mar 27 22:06:46 2020 +0100
@@ -137,7 +137,7 @@
JEdit_Lib.buffer_lock(buffer) {
val rendering = get_rendering()
- for (i <- 0 until physical_lines.length) {
+ for (i <- physical_lines.indices) {
if (physical_lines(i) != -1) {
val line_range = Text.Range(start(i), end(i))
@@ -241,7 +241,7 @@
text_area.revalidate()
text_area.repaint()
Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
- foreach(text_area.addStructureMatcher(_))
+ foreach(text_area.addStructureMatcher)
session.raw_edits += main
session.commands_changed += main
}
@@ -253,7 +253,7 @@
session.raw_edits -= main
session.commands_changed -= main
Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
- foreach(text_area.removeStructureMatcher(_))
+ foreach(text_area.removeStructureMatcher)
text_overview.foreach(_.revoke())
text_overview.foreach(text_area.removeLeftOfScrollBar(_))
text_area.removeCaretListener(caret_listener)
--- a/src/Tools/jEdit/src/isabelle.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Mar 27 22:06:46 2020 +0100
@@ -406,8 +406,8 @@
private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
{
- s1.foreach(text_area.userInput(_))
- s2.foreach(text_area.userInput(_))
+ s1.foreach(text_area.userInput)
+ s2.foreach(text_area.userInput)
s2.foreach(_ => text_area.goToPrevCharacter(false))
}
--- a/src/Tools/jEdit/src/isabelle_options.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Fri Mar 27 22:06:46 2020 +0100
@@ -39,7 +39,7 @@
class Isabelle_Options1 extends Isabelle_Options("isabelle-general")
{
- val options = PIDE.options
+ val options: JEdit_Options = PIDE.options
private val predefined =
List(JEdit_Sessions.logic_selector(options, false),
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Mar 27 22:06:46 2020 +0100
@@ -53,11 +53,11 @@
}
override def getLongString: String = _name
override def getName: String = _name
- override def setName(name: String) = _name = name
+ override def setName(name: String): Unit = _name = name
override def getStart: Position = _start
- override def setStart(start: Position) = _start = start
+ override def setStart(start: Position): Unit = _start = start
override def getEnd: Position = _end
- override def setEnd(end: Position) = _end = end
+ override def setEnd(end: Position): Unit = _end = end
override def toString: String = _name
}
@@ -148,19 +148,19 @@
class Isabelle_Sidekick_Default extends
Isabelle_Sidekick_Structure("isabelle",
- PIDE.resources.theory_node_name, Document_Structure.parse_sections _)
+ PIDE.resources.theory_node_name, Document_Structure.parse_sections)
class Isabelle_Sidekick_Context extends
Isabelle_Sidekick_Structure("isabelle-context",
- PIDE.resources.theory_node_name, Document_Structure.parse_blocks _)
+ PIDE.resources.theory_node_name, Document_Structure.parse_blocks)
class Isabelle_Sidekick_Options extends
Isabelle_Sidekick_Structure("isabelle-options",
- _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections _)
+ _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections)
class Isabelle_Sidekick_Root extends
Isabelle_Sidekick_Structure("isabelle-root",
- _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections _)
+ _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections)
class Isabelle_Sidekick_ML extends
Isabelle_Sidekick_Structure("isabelle-ml",
@@ -257,7 +257,7 @@
case _ =>
}
offset += line.length + 1
- if (!line.forall(Character.isSpaceChar(_))) end_offset = offset
+ if (!line.forall(Character.isSpaceChar)) end_offset = offset
}
if (!stopped) { close2; close1 }
--- a/src/Tools/jEdit/src/isabelle_vfs.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle_vfs.scala Fri Mar 27 22:06:46 2020 +0100
@@ -77,7 +77,7 @@
else {
val files = _listFiles(vfs_session, parent, component)
if (files == null) null
- else files.find(_.getPath == url) getOrElse null
+ else files.find(_.getPath == url).orNull
}
}
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Mar 27 22:06:46 2020 +0100
@@ -202,7 +202,7 @@
case doc: Doc.Text_File if doc.name == name => doc.path
case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
new Hyperlink {
- override val external = !path.is_file
+ override val external: Boolean = !path.is_file
def follow(view: View): Unit = goto_doc(view, path)
override def toString: String = "doc " + quote(name)
})
--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Mar 27 22:06:46 2020 +0100
@@ -160,7 +160,7 @@
else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null)
def jedit_text_areas(): Iterator[JEditTextArea] =
- jedit_views().flatMap(jedit_text_areas(_))
+ jedit_views().flatMap(jedit_text_areas)
def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
jedit_text_areas().filter(_.getBuffer == buffer)
@@ -319,8 +319,8 @@
def string_width(s: String): Double =
painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
- val unit = string_width(Symbol.space) max 1.0
- val average = string_width("mix") / (3 * unit)
+ val unit: Double = string_width(Symbol.space) max 1.0
+ val average: Double = string_width("mix") / (3 * unit)
def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
}
--- a/src/Tools/jEdit/src/jedit_options.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala Fri Mar 27 22:06:46 2020 +0100
@@ -129,7 +129,7 @@
case None => if (filter(opt.name)) List(make_component(opt)) else Nil
}
value.sections.sortBy(_._1).map(
- { case (a, opts) => (a, opts.sortBy(_.title("jedit")).flatMap(mk_component _)) })
+ { case (a, opts) => (a, opts.sortBy(_.title("jedit")).flatMap(mk_component)) })
.filterNot(_._2.isEmpty)
}
}
--- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Mar 27 22:06:46 2020 +0100
@@ -300,11 +300,11 @@
def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[XML.Body]] =
{
val elements = if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements
- tooltips(elements, range).map(info => info.map(Pretty.fbreaks(_)))
+ tooltips(elements, range).map(info => info.map(Pretty.fbreaks))
}
- lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
- lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
+ lazy val tooltip_close_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
+ lazy val tooltip_detach_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
/* gutter */
@@ -378,7 +378,7 @@
else
snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ =>
{
- case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color(_))
+ case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color)
})
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Fri Mar 27 22:06:46 2020 +0100
@@ -37,7 +37,7 @@
/* document node name */
def node_name(path: String): Document.Node.Name =
- JEdit_Lib.check_file(path).flatMap(find_theory(_)) getOrElse {
+ JEdit_Lib.check_file(path).flatMap(find_theory) getOrElse {
val vfs = VFSManager.getVFSForPath(path)
val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Mar 27 22:06:46 2020 +0100
@@ -136,11 +136,11 @@
def session_start(options0: Options)
{
val options = session_options(options0)
+ val store = Sessions.store(options)
- Isabelle_Process.start(PIDE.session, options,
- sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure),
+ Isabelle_Process(PIDE.session, options,
+ PIDE.resources.session_base_info.sessions_structure, store,
logic = PIDE.resources.session_name,
- store = Some(Sessions.store(options)),
modes =
(space_explode(',', options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,
--- a/src/Tools/jEdit/src/output_dockable.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Fri Mar 27 22:06:46 2020 +0100
@@ -32,7 +32,7 @@
val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
- override def detach_operation = pretty_text_area.detach_operation
+ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
private def handle_resize()
@@ -58,7 +58,7 @@
}
val new_output =
- if (!restriction.isDefined || restriction.get.contains(command))
+ if (restriction.isEmpty || restriction.get.contains(command))
Rendering.output_messages(results)
else current_output
--- a/src/Tools/jEdit/src/plugin.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Mar 27 22:06:46 2020 +0100
@@ -150,7 +150,7 @@
}
else Nil
- (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt(_))
+ (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt)
}
if (required_files.nonEmpty) {
try {
@@ -184,7 +184,7 @@
if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
lazy val file_watcher: File_Watcher =
- File_Watcher(file_watcher_action _, options.seconds("editor_load_delay"))
+ File_Watcher(file_watcher_action, options.seconds("editor_load_delay"))
/* session phase */
@@ -460,11 +460,11 @@
completion_history.load()
spell_checker.update(options.value)
- JEdit_Lib.jedit_views.foreach(init_title(_))
+ JEdit_Lib.jedit_views.foreach(init_title)
isabelle.jedit_base.Syntax_Style.set_style_extender(Syntax_Style.Extender)
init_mode_provider()
- JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
+ JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init)
http_server.start
@@ -489,7 +489,7 @@
isabelle.jedit_base.Syntax_Style.dummy_style_extender()
exit_mode_provider()
- JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
+ JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit)
if (startup_failure.isEmpty) {
options.value.save_prefs()
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Mar 27 22:06:46 2020 +0100
@@ -146,7 +146,7 @@
}
def dismiss_descendant(parent: JComponent): Unit =
- descendant(parent).foreach(dismiss(_))
+ descendant(parent).foreach(dismiss)
def dismissed_all(): Boolean =
{
@@ -203,7 +203,7 @@
/* text area */
- val pretty_text_area =
+ val pretty_text_area: Pretty_Text_Area =
new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) {
override def get_background() = Some(rendering.tooltip_color)
}
@@ -262,7 +262,7 @@
val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
val lines =
XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
- (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
+ (n: Int, s: String) => n + s.iterator.count(_ == '\n'))
val h = painter.getLineHeight * lines + geometry.deco_height
val margin1 =
--- a/src/Tools/jEdit/src/query_dockable.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Fri Mar 27 22:06:46 2020 +0100
@@ -302,7 +302,7 @@
select_operation()
set_content(operations_pane)
- override def detach_operation =
+ override def detach_operation: Option[() => Unit] =
get_operation() match {
case None => None
case Some(op) => op.pretty_text_area.detach_operation
--- a/src/Tools/jEdit/src/rich_text_area.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Mar 27 22:06:46 2020 +0100
@@ -159,15 +159,15 @@
private val highlight_area =
new Active_Area[Color](
- (rendering: JEdit_Rendering) => rendering.highlight _, None)
+ (rendering: JEdit_Rendering) => rendering.highlight, None)
private val hyperlink_area =
new Active_Area[PIDE.editor.Hyperlink](
- (rendering: JEdit_Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR))
+ (rendering: JEdit_Rendering) => rendering.hyperlink, Some(Cursor.HAND_CURSOR))
private val active_area =
new Active_Area[XML.Elem](
- (rendering: JEdit_Rendering) => rendering.active _, Some(Cursor.DEFAULT_CURSOR))
+ (rendering: JEdit_Rendering) => rendering.active, Some(Cursor.DEFAULT_CURSOR))
private val active_areas =
List((highlight_area, true), (hyperlink_area, true), (active_area, false))
@@ -292,7 +292,7 @@
robust_rendering { rendering =>
val fm = text_area.getPainter.getFontMetrics
- for (i <- 0 until physical_lines.length) {
+ for (i <- physical_lines.indices) {
if (physical_lines(i) != -1) {
val line_range = Text.Range(start(i), end(i) min buffer.getLength)
@@ -479,7 +479,7 @@
((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
}
- for (i <- 0 until physical_lines.length) {
+ for (i <- physical_lines.indices) {
val line = physical_lines(i)
if (line != -1) {
val line_range = Text.Range(start(i), end(i) min buffer.getLength)
@@ -525,7 +525,7 @@
{
robust_rendering { rendering =>
val search_pattern = get_search_pattern()
- for (i <- 0 until physical_lines.length) {
+ for (i <- physical_lines.indices) {
if (physical_lines(i) != -1) {
val line_range = Text.Range(start(i), end(i) min buffer.getLength)
--- a/src/Tools/jEdit/src/scala_console.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Fri Mar 27 22:06:46 2020 +0100
@@ -30,7 +30,7 @@
def find_jars(start: String): List[String] =
if (start != null)
File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
- map(File.absolute_name(_))
+ map(File.absolute_name)
else Nil
val initial_class_path =
--- a/src/Tools/jEdit/src/session_build.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Fri Mar 27 22:06:46 2020 +0100
@@ -40,7 +40,7 @@
private class Dialog(view: View) extends JDialog(view)
{
- val options = PIDE.options.value
+ val options: Options = PIDE.options.value
/* text */
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Mar 27 22:06:46 2020 +0100
@@ -30,7 +30,7 @@
val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
- override def detach_operation = pretty_text_area.detach_operation
+ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
/* query operation */
@@ -50,7 +50,7 @@
}
private val sledgehammer =
- new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _,
+ new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status,
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
--- a/src/Tools/jEdit/src/state_dockable.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Fri Mar 27 22:06:46 2020 +0100
@@ -29,7 +29,7 @@
val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
- override def detach_operation = pretty_text_area.detach_operation
+ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
private val print_state =
new Query_Operation(PIDE.editor, view, "print_state", _ => (),
--- a/src/Tools/jEdit/src/symbols_dockable.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Fri Mar 27 22:06:46 2020 +0100
@@ -174,7 +174,7 @@
}
for (page <- pages)
- page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
+ page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize))
}
set_content(group_tabs)
@@ -200,7 +200,7 @@
}
case _ =>
})
- comp.revalidate
+ comp.revalidate()
comp.repaint()
}
case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke()
--- a/src/Tools/jEdit/src/syntax_style.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala Fri Mar 27 22:06:46 2020 +0100
@@ -99,9 +99,9 @@
}
private def control_style(sym: String): Option[Byte => Byte] =
- if (sym == Symbol.sub_decoded) Some(subscript(_))
- else if (sym == Symbol.sup_decoded) Some(superscript(_))
- else if (sym == Symbol.bold_decoded) Some(bold(_))
+ if (sym == Symbol.sub_decoded) Some(subscript)
+ else if (sym == Symbol.sup_decoded) Some(superscript)
+ else if (sym == Symbol.bold_decoded) Some(bold)
else None
def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
--- a/src/Tools/jEdit/src/text_structure.scala Fri Mar 27 12:28:05 2020 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala Fri Mar 27 22:06:46 2020 +0100
@@ -21,7 +21,7 @@
class Navigator(syntax: Outer_Syntax, buffer: JEditBuffer, comments: Boolean)
{
- val limit = PIDE.options.value.int("jedit_structure_limit") max 0
+ val limit: Int = PIDE.options.value.int("jedit_structure_limit") max 0
def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
{
@@ -137,7 +137,7 @@
else i })
def indent_extra: Int =
- if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
+ if (prev_span.exists(keywords.is_quasi_command)) indent_size
else 0
val indent =