--- a/etc/settings Thu Mar 04 18:38:56 2021 +0100
+++ b/etc/settings Fri Mar 05 08:22:34 2021 +0100
@@ -16,7 +16,7 @@
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
-ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:11 -J-Xms512m -J-Xmx4g -J-Xss16m"
+ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -Wconf:cat=other-match-analysis:silent -feature -deprecation -target:11 -J-Xms512m -J-Xmx4g -J-Xss16m"
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
--- a/src/HOL/Analysis/Affine.thy Thu Mar 04 18:38:56 2021 +0100
+++ b/src/HOL/Analysis/Affine.thy Fri Mar 05 08:22:34 2021 +0100
@@ -1612,26 +1612,29 @@
assumes "\<not> affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
shows "(affine hull t) \<inter> (affine hull u) = {}"
proof -
- have "finite s" using assms by (simp add: aff_independent_finite)
- then have "finite t" "finite u" using assms finite_subset by blast+
- { fix y
- assume yt: "y \<in> affine hull t" and yu: "y \<in> affine hull u"
- then obtain a b
- where a1 [simp]: "sum a t = 1" and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) t = y"
- and [simp]: "sum b u = 1" "sum (\<lambda>v. b v *\<^sub>R v) u = y"
+ from assms(1) have "finite s"
+ by (simp add: aff_independent_finite)
+ with assms(2,3) have "finite t" "finite u"
+ by (blast intro: finite_subset)+
+ have False if "y \<in> affine hull t" and "y \<in> affine hull u" for y
+ proof -
+ from that obtain a b
+ where a1 [simp]: "sum a t = 1"
+ and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) t = y"
+ and [simp]: "sum b u = 1" "sum (\<lambda>v. b v *\<^sub>R v) u = y"
by (auto simp: affine_hull_finite \<open>finite t\<close> \<open>finite u\<close>)
define c where "c x = (if x \<in> t then a x else if x \<in> u then -(b x) else 0)" for x
- have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u" using assms by auto
+ from assms(2,3,4) have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u"
+ by auto
have "sum c s = 0"
by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite s\<close> sum_negf)
moreover have "\<not> (\<forall>v\<in>s. c v = 0)"
by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum.neutral zero_neq_one)
moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
- by (simp add: c_def if_smult sum_negf
- comm_monoid_add_class.sum.If_cases \<open>finite s\<close>)
- ultimately have False
- using assms \<open>finite s\<close> by (auto simp: affine_dependent_explicit)
- }
+ by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases \<open>finite s\<close>)
+ ultimately show ?thesis
+ using assms(1) \<open>finite s\<close> by (auto simp: affine_dependent_explicit)
+ qed
then show ?thesis by blast
qed
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Mar 04 18:38:56 2021 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Mar 05 08:22:34 2021 +0100
@@ -3729,7 +3729,6 @@
then have eba8: "(e * (b-a)) / 8 > 0"
using ab by (auto simp add: field_simps)
note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt, THEN conjunct2, rule_format]
- thm derf_exp
have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
by (simp add: bounded_linear_scaleR_left)
have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
--- a/src/HOL/Tools/Nitpick/kodkod.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.scala Fri Mar 05 08:22:34 2021 +0100
@@ -96,7 +96,7 @@
/* main */
try {
- val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream))
+ val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream()))
val parser =
KodkodiParser.create(context, executor,
false, solve_all, prove, max_solutions, cleanup_inst, lexer)
@@ -114,7 +114,7 @@
try { parser.problems() }
catch { case exn: RecognitionException => parser.reportError(exn) }
- timeout_request.foreach(_.cancel)
+ timeout_request.foreach(_.cancel())
if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) {
context.error("Error: trailing tokens")
--- a/src/Pure/Admin/afp.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/afp.scala Fri Mar 05 08:22:34 2021 +0100
@@ -136,7 +136,7 @@
}
val entries_map =
- (SortedMap.empty[String, AFP.Entry] /: entries)({ case (m, e) => m + (e.name -> e) })
+ entries.foldLeft(SortedMap.empty[String, AFP.Entry]) { case (m, e) => m + (e.name -> e) }
val extra_metadata =
(for ((name, _) <- entry_metadata.iterator if !entries_map.isDefinedAt(name)) yield name).
@@ -153,8 +153,9 @@
/* sessions */
val sessions_map: SortedMap[String, AFP.Entry] =
- (SortedMap.empty[String, AFP.Entry] /: entries)(
- { case (m1, e) => (m1 /: e.sessions)({ case (m2, s) => m2 + (s -> e) }) })
+ entries.foldLeft(SortedMap.empty[String, AFP.Entry]) {
+ case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e) }
+ }
val sessions: List[String] = entries.flatMap(_.sessions)
@@ -171,22 +172,25 @@
lazy val entries_graph: Graph[String, Unit] =
{
val session_entries =
- (Map.empty[String, String] /: entries) {
- case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) }
+ entries.foldLeft(Map.empty[String, String]) {
+ case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e.name) }
}
- (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
- val e1 = entry.name
- (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) =>
- (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
- try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
- catch {
- case exn: Graph.Cycles[_] =>
- error(cat_lines(exn.cycles.map(cycle =>
- "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
- " due to session " + quote(s))))
- }
+ entries.foldLeft(Graph.empty[String, Unit]) {
+ case (g, entry) =>
+ val e1 = entry.name
+ sessions_deps(entry).foldLeft(g.default_node(e1, ())) {
+ case (g1, s) =>
+ session_entries.get(s).filterNot(_ == e1).foldLeft(g1) {
+ case (g2, e2) =>
+ try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
+ catch {
+ case exn: Graph.Cycles[_] =>
+ error(cat_lines(exn.cycles.map(cycle =>
+ "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
+ " due to session " + quote(s))))
+ }
+ }
}
- }
}
}
--- a/src/Pure/Admin/build_csdp.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/build_csdp.scala Fri Mar 05 08:22:34 2021 +0100
@@ -31,7 +31,7 @@
def change_line(line: String, entry: (String, String)): String =
line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2)
File.change(path, s =>
- split_lines(s).map(line => (line /: changed)(change_line)).mkString("\n"))
+ split_lines(s).map(line => changed.foldLeft(line)(change_line)).mkString("\n"))
}
}
--- a/src/Pure/Admin/build_history.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/build_history.scala Fri Mar 05 08:22:34 2021 +0100
@@ -519,7 +519,7 @@
cat_lines(for ((_, log_path) <- results) yield log_path.implode))
}
- val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
+ val rc = results.foldLeft(0) { case (rc, (res, _)) => rc max res.rc }
if (rc != 0 && exit_code) sys.exit(rc)
}
}
--- a/src/Pure/Admin/build_status.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/build_status.scala Fri Mar 05 08:22:34 2021 +0100
@@ -429,11 +429,13 @@
entry.stored_heap.toString).mkString(" "))))
val max_time =
- ((0.0 /: session.finished_entries){ case (m, entry) =>
- m.max(entry.timing.elapsed.minutes).
- max(entry.timing.resources.minutes).
- max(entry.ml_timing.elapsed.minutes).
- max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
+ (session.finished_entries.foldLeft(0.0) {
+ case (m, entry) =>
+ m.max(entry.timing.elapsed.minutes).
+ max(entry.timing.resources.minutes).
+ max(entry.ml_timing.elapsed.minutes).
+ max(entry.ml_timing.resources.minutes)
+ } max 0.1) * 1.1
val timing_range = "[0:" + max_time + "]"
def gnuplot(plot_name: String, plots: List[String], range: String): Image =
--- a/src/Pure/Admin/ci_profile.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/ci_profile.scala Fri Mar 05 08:22:34 2021 +0100
@@ -56,7 +56,7 @@
case session if group.forall(results.info(session).groups.contains(_)) =>
results(session).timing
}
- (Timing.zero /: timings)(_ + _)
+ timings.foldLeft(Timing.zero)(_ + _)
}
private def with_documents(options: Options): Options =
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Mar 05 08:22:34 2021 +0100
@@ -183,9 +183,9 @@
if (historic || items.exists(_.known_versions(rev, afp_rev))) {
val longest_run =
- (List.empty[Item] /: runs)({ case (item1, item2) =>
- if (item1.length >= item2.length) item1 else item2
- })
+ runs.foldLeft(List.empty[Item]) {
+ case (item1, item2) => if (item1.length >= item2.length) item1 else item2
+ }
if (longest_run.isEmpty) None
else Some(longest_run(longest_run.length / 2).versions)
}
--- a/src/Pure/Concurrent/delay.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Concurrent/delay.scala Fri Mar 05 08:22:34 2021 +0100
@@ -37,7 +37,7 @@
{
val new_run =
running match {
- case Some(request) => if (first) false else { request.cancel; true }
+ case Some(request) => if (first) false else { request.cancel(); true }
case None => true
}
if (new_run)
@@ -47,7 +47,7 @@
def revoke(): Unit = synchronized
{
running match {
- case Some(request) => request.cancel; running = None
+ case Some(request) => request.cancel(); running = None
case None =>
}
}
@@ -57,7 +57,7 @@
running match {
case Some(request) =>
val alt_time = Time.now() + alt_delay
- if (request.time < alt_time && request.cancel) {
+ if (request.time < alt_time && request.cancel()) {
running = Some(Event_Timer.request(alt_time)(run))
}
case None =>
--- a/src/Pure/Concurrent/event_timer.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Concurrent/event_timer.scala Fri Mar 05 08:22:34 2021 +0100
@@ -19,7 +19,7 @@
final class Request private[Event_Timer](val time: Time, val repeat: Option[Time], task: TimerTask)
{
- def cancel: Boolean = task.cancel
+ def cancel(): Boolean = task.cancel()
}
def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request =
--- a/src/Pure/Concurrent/future.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Concurrent/future.scala Fri Mar 05 08:22:34 2021 +0100
@@ -38,7 +38,7 @@
def join_result: Exn.Result[A]
def join: A = Exn.release(join_result)
def map[B](f: A => B): Future[B] = Future.fork { f(join) }
- def cancel: Unit
+ def cancel(): Unit
override def toString: String =
peek match {
@@ -61,7 +61,7 @@
{
val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
def join_result: Exn.Result[A] = peek.get
- def cancel: Unit = {}
+ def cancel(): Unit = {}
}
@@ -93,7 +93,7 @@
if (do_run) {
val result = Exn.capture(body)
status.change(_ => Terminated)
- status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result))
+ status.change(_ => Finished(if (Thread.interrupted()) Exn.Exn(Exn.Interrupt()) else result))
}
}
private val task = Isabelle_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
@@ -107,11 +107,11 @@
}
}
- def cancel =
+ def cancel(): Unit =
{
status.change {
case Ready => task.cancel(false); Finished(Exn.Exn(Exn.Interrupt()))
- case st @ Running(thread) => thread.interrupt; st
+ case st @ Running(thread) => thread.interrupt(); st
case st => st
}
}
@@ -133,7 +133,7 @@
def fulfill(x: A): Unit = fulfill_result(Exn.Res(x))
- def cancel: Unit =
+ def cancel(): Unit =
state.change(st => if (st.isEmpty) Some(Exn.Exn(Exn.Interrupt())) else st)
}
@@ -157,5 +157,5 @@
def peek: Option[Exn.Result[A]] = result.peek
def join_result: Exn.Result[A] = result.join_result
- def cancel: Unit = thread.interrupt
+ def cancel(): Unit = thread.interrupt()
}
--- a/src/Pure/Concurrent/isabelle_thread.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.scala Fri Mar 05 08:22:34 2021 +0100
@@ -174,7 +174,7 @@
// non-synchronized, only changed on self-thread
@volatile private var handler = Isabelle_Thread.Interrupt_Handler.interruptible
- override def interrupt: Unit = handler(thread)
+ override def interrupt(): Unit = handler(thread)
def interrupt_handler[A](new_handler: Isabelle_Thread.Interrupt_Handler)(body: => A): A =
if (new_handler == null) body
@@ -184,12 +184,12 @@
val old_handler = handler
handler = new_handler
try {
- if (clear_interrupt) interrupt
+ if (clear_interrupt) interrupt()
body
}
finally {
handler = old_handler
- if (clear_interrupt) interrupt
+ if (clear_interrupt) interrupt()
}
}
}
--- a/src/Pure/Concurrent/par_list.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Concurrent/par_list.scala Fri Mar 05 08:22:34 2021 +0100
@@ -19,7 +19,7 @@
state.change { case (futures, canceled) =>
if (!canceled) {
for ((future, i) <- futures.iterator.zipWithIndex if i != self)
- future.cancel
+ future.cancel()
}
(futures, true)
}
--- a/src/Pure/GUI/gui.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/GUI/gui.scala Fri Mar 05 08:22:34 2021 +0100
@@ -22,10 +22,10 @@
def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.install()
- def current_laf(): String = UIManager.getLookAndFeel.getClass.getName()
+ def current_laf: String = UIManager.getLookAndFeel.getClass.getName()
- def is_macos_laf(): Boolean =
- Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf()
+ def is_macos_laf: Boolean =
+ Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf
class Look_And_Feel(laf: LookAndFeel) extends Isabelle_System.Service
{
--- a/src/Pure/General/completion.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/completion.scala Fri Mar 05 08:22:34 2021 +0100
@@ -32,7 +32,7 @@
{
def empty(range: Text.Range): Result = Result(range, "", false, Nil)
def merge(history: History, results: Option[Result]*): Option[Result] =
- ((None: Option[Result]) /: results)({
+ results.foldLeft(None: Option[Result]) {
case (result1, None) => result1
case (None, result2) => result2
case (result1 @ Some(res1), Some(res2)) =>
@@ -41,7 +41,7 @@
val items = (res1.items ::: res2.items).sorted(history.ordering)
Some(Result(res1.range, res1.original, false, items))
}
- })
+ }
}
sealed case class Result(
@@ -78,7 +78,7 @@
}
}
else Nil
- (empty /: content)(_ + _)
+ content.foldLeft(empty)(_ + _)
}
}
@@ -356,7 +356,7 @@
def add_keywords(names: List[String]): Completion =
{
- val keywords1 = (keywords /: names) { case (ks, k) => if (ks(k)) ks else ks + k }
+ val keywords1 = names.foldLeft(keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
if (keywords eq keywords1) this
else new Completion(keywords1, words_lex, words_map, abbrevs_lex, abbrevs_map)
}
@@ -386,7 +386,7 @@
}
def add_abbrevs(abbrevs: List[(String, String)]): Completion =
- (this /: abbrevs)(_.add_abbrev(_))
+ abbrevs.foldLeft(this)(_.add_abbrev(_))
private def add_abbrev(abbrev: (String, String)): Completion =
abbrev match {
--- a/src/Pure/General/exn.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/exn.scala Fri Mar 05 08:22:34 2021 +0100
@@ -102,9 +102,9 @@
def apply(): Throwable = new InterruptedException("Interrupt")
def unapply(exn: Throwable): Boolean = is_interrupt(exn)
- def dispose(): Unit = Thread.interrupted
- def expose(): Unit = if (Thread.interrupted) throw apply()
- def impose(): Unit = Thread.currentThread.interrupt
+ def dispose(): Unit = Thread.interrupted()
+ def expose(): Unit = if (Thread.interrupted()) throw apply()
+ def impose(): Unit = Thread.currentThread.interrupt()
val return_code = 130
}
--- a/src/Pure/General/file.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/file.scala Fri Mar 05 08:22:34 2021 +0100
@@ -199,7 +199,7 @@
val output = new StringBuilder(100)
var c = -1
while ({ c = reader.read; c != -1 }) output += c.toChar
- reader.close
+ reader.close()
output.toString
}
@@ -233,7 +233,7 @@
progress(line.get)
result += line.get
}
- reader.close
+ reader.close()
result.toList
}
--- a/src/Pure/General/file_watcher.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/file_watcher.scala Fri Mar 05 08:22:34 2021 +0100
@@ -72,14 +72,14 @@
st.dirs.get(dir) match {
case None => st
case Some(key) =>
- key.cancel
+ key.cancel()
st.copy(dirs = st.dirs - dir)
})
override def purge(retain: Set[JFile]): Unit =
state.change(st =>
st.copy(dirs = st.dirs --
- (for ((dir, key) <- st.dirs.iterator if !retain(dir)) yield { key.cancel; dir })))
+ (for ((dir, key) <- st.dirs.iterator if !retain(dir)) yield { key.cancel(); dir })))
/* changed directory entries */
@@ -105,7 +105,7 @@
key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala
val remove = if (key.reset) None else Some(dir)
val changed =
- (Set.empty[JFile] /: events.iterator) {
+ events.iterator.foldLeft(Set.empty[JFile]) {
case (set, event) => set + dir.toPath.resolve(event.context).toFile
}
(remove, changed)
@@ -127,9 +127,9 @@
override def shutdown(): Unit =
{
- watcher_thread.interrupt
+ watcher_thread.interrupt()
watcher_thread.join
- delay_changed.revoke
+ delay_changed.revoke()
}
}
}
--- a/src/Pure/General/graph.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/graph.scala Fri Mar 05 08:22:34 2021 +0100
@@ -33,10 +33,16 @@
symmetric: Boolean = false)(implicit ord: Ordering[Key]): Graph[Key, A] =
{
val graph1 =
- (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
+ entries.foldLeft(empty[Key, A](ord)) {
+ case (graph, ((x, info), _)) => graph.new_node(x, info)
+ }
val graph2 =
- (graph1 /: entries) { case (graph, ((x, _), ys)) =>
- (graph /: ys)({ case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) }) }
+ entries.foldLeft(graph1) {
+ case (graph, ((x, _), ys)) =>
+ ys.foldLeft(graph) {
+ case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y)
+ }
+ }
graph2
}
@@ -119,8 +125,8 @@
{
def reach(length: Long)(rs: Map[Key, Long], x: Key): Map[Key, Long] =
if (rs.get(x) match { case Some(n) => n >= length case None => false }) rs
- else ((rs + (x -> length)) /: next(x))(reach(length + count(x)))
- (Map.empty[Key, Long] /: xs)(reach(0))
+ else next(x).foldLeft(rs + (x -> length))(reach(length + count(x)))
+ xs.foldLeft(Map.empty[Key, Long])(reach(0))
}
def node_height(count: Key => Long): Map[Key, Long] =
reachable_length(count, imm_preds, maximals)
@@ -138,7 +144,7 @@
{
val (n, rs) = res
if (rs.contains(x)) res
- else ((n + count(x), rs + x) /: next(x))(reach)
+ else next(x).foldLeft((n + count(x), rs + x))(reach)
}
@tailrec def reachs(size: Long, rs: Keys, rest: List[Key]): Keys =
@@ -162,8 +168,8 @@
if (r_set(x)) reached
else {
val (rs1, r_set1) =
- if (rev) ((rs, r_set + x) /: next(x))({ case (b, a) => reach(a, b) })
- else (next(x) :\ (rs, r_set + x))(reach)
+ if (rev) next(x).foldLeft((rs, r_set + x)) { case (b, a) => reach(a, b) }
+ else next(x).foldRight((rs, r_set + x))(reach)
(x :: rs1, r_set1)
}
}
@@ -173,7 +179,7 @@
val (rs, r_set1) = reach(x, (Nil, r_set))
(rs :: rss, r_set1)
}
- ((List.empty[List[Key]], empty_keys) /: xs)(reachs)
+ xs.foldLeft((List.empty[List[Key]], empty_keys))(reachs)
}
/*immediate*/
@@ -195,12 +201,14 @@
/* minimal and maximal elements */
def minimals: List[Key] =
- (List.empty[Key] /: rep) {
- case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms }
+ rep.foldLeft(List.empty[Key]) {
+ case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms
+ }
def maximals: List[Key] =
- (List.empty[Key] /: rep) {
- case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms }
+ rep.foldLeft(List.empty[Key]) {
+ case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms
+ }
def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
@@ -231,11 +239,11 @@
{
val (preds, succs) = get_entry(x)._2
new Graph[Key, A](
- (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x)))
+ succs.foldLeft(preds.foldLeft(rep - x)(del_adjacent(false, x)))(del_adjacent(true, x)))
}
def restrict(pred: Key => Boolean): Graph[Key, A] =
- (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
+ iterator.foldLeft(this) { case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
def exclude(pred: Key => Boolean): Graph[Key, A] = restrict(name => !pred(name))
@@ -283,7 +291,7 @@
val (_, x_set) = reachable(imm_succs, List(x))
def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] =
if (x == z) (z :: path) :: ps
- else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path))
+ else irreducible_preds(x_set, path, z).foldLeft(ps)(paths(z :: path))
if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y)
}
@@ -298,7 +306,7 @@
graph
}
- def transitive_closure: Graph[Key, A] = (this /: keys_iterator)(_.transitive_step(_))
+ def transitive_closure: Graph[Key, A] = keys_iterator.foldLeft(this)(_.transitive_step(_))
def transitive_reduction_acyclic: Graph[Key, A] =
{
@@ -328,7 +336,7 @@
}
def add_deps_acyclic(y: Key, xs: List[Key]): Graph[Key, A] =
- (this /: xs)(_.add_edge_acyclic(_, y))
+ xs.foldLeft(this)(_.add_edge_acyclic(_, y))
def topological_order: List[Key] = all_succs(minimals)
}
--- a/src/Pure/General/graph_display.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/graph_display.scala Fri Mar 05 08:22:34 2021 +0100
@@ -43,14 +43,15 @@
def build_graph(entries: List[Entry]): Graph =
{
val node =
- (Map.empty[String, Node] /: entries) {
+ entries.foldLeft(Map.empty[String, Node]) {
case (m, ((ident, (name, _)), _)) => m + (ident -> Node(name, ident))
}
- (((empty_graph /: entries) {
+ entries.foldLeft(
+ entries.foldLeft(empty_graph) {
case (g, ((ident, (_, content)), _)) => g.new_node(node(ident), content)
- }) /: entries) {
+ }) {
case (g1, ((ident, _), parents)) =>
- (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
+ parents.foldLeft(g1) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
}
}
--- a/src/Pure/General/http.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/http.scala Fri Mar 05 08:22:34 2021 +0100
@@ -109,8 +109,8 @@
def += (handler: Handler): Unit = http_server.createContext(handler.root, handler.handler)
def -= (handler: Handler): Unit = http_server.removeContext(handler.root)
- def start: Unit = http_server.start
- def stop: Unit = http_server.stop(0)
+ def start(): Unit = http_server.start
+ def stop(): Unit = http_server.stop(0)
def address: InetSocketAddress = http_server.getAddress
def url: String = "http://" + address.getHostName + ":" + address.getPort
--- a/src/Pure/General/linear_set.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/linear_set.scala Fri Mar 05 08:22:34 2021 +0100
@@ -18,7 +18,8 @@
private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]]
- def from[A](entries: IterableOnce[A]): Linear_Set[A] = (empty[A] /: entries)(_.incl(_))
+ def from[A](entries: IterableOnce[A]): Linear_Set[A] =
+ entries.iterator.foldLeft(empty[A])(_.incl(_))
override def newBuilder[A]: mutable.Builder[A, Linear_Set[A]] = new Builder[A]
private class Builder[A] extends mutable.Builder[A, Linear_Set[A]]
@@ -83,7 +84,7 @@
}
def append_after(hook: Option[A], elems: Iterable[A]): Linear_Set[A] = // FIXME reverse fold
- ((hook, this) /: elems) {
+ elems.foldLeft((hook, this)) {
case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
}._2
--- a/src/Pure/General/mailman.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/mailman.scala Fri Mar 05 08:22:34 2021 +0100
@@ -55,7 +55,7 @@
Some(path)
}
}
- finally { connection.getInputStream.close }
+ finally { connection.getInputStream.close() }
})
}
}
--- a/src/Pure/General/mercurial.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/mercurial.scala Fri Mar 05 08:22:34 2021 +0100
@@ -144,11 +144,11 @@
val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
val log_result =
log(template = """node: {node|short} {p1node|short} {p2node|short}\n""")
- (Graph.string[Unit] /: split_lines(log_result)) {
+ split_lines(log_result).foldLeft(Graph.string[Unit]) {
case (graph, Node(x, y, z)) =>
val deps = List(y, z).filterNot(s => s.forall(_ == '0'))
- val graph1 = (graph /: (x :: deps))(_.default_node(_, ()))
- (graph1 /: deps)({ case (g, dep) => g.add_edge(dep, x) })
+ val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ()))
+ deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) })
case (graph, _) => graph
}
}
--- a/src/Pure/General/multi_map.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/multi_map.scala Fri Mar 05 08:22:34 2021 +0100
@@ -17,7 +17,7 @@
def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
def from[A, B](entries: IterableOnce[(A, B)]): Multi_Map[A, B] =
- (empty[A, B] /: entries)({ case (m, (a, b)) => m.insert(a, b) })
+ entries.iterator.foldLeft(empty[A, B]) { case (m, (a, b)) => m.insert(a, b) }
override def newBuilder[A, B]: mutable.Builder[(A, B), Multi_Map[A, B]] = new Builder[A, B]
private class Builder[A, B] extends mutable.Builder[(A, B), Multi_Map[A, B]]
@@ -63,8 +63,8 @@
if (this eq other) this
else if (isEmpty) other
else
- (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) {
- case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
+ other.rep.iterator.foldLeft(this.asInstanceOf[Multi_Map[A, B1]]) {
+ case (m1, (a, bs)) => bs.foldRight(m1) { case (b, m2) => m2.insert(a, b) }
}
--- a/src/Pure/General/path.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/path.scala Fri Mar 05 08:22:34 2021 +0100
@@ -54,7 +54,7 @@
}
private def norm_elems(elems: List[Elem]): List[Elem] =
- (elems :\ (Nil: List[Elem]))(apply_elem)
+ elems.foldRight(List.empty[Elem])(apply_elem)
private def implode_elem(elem: Elem, short: Boolean): String =
elem match {
@@ -146,10 +146,10 @@
def check_case_insensitive(paths: List[Path]): Unit =
{
val table =
- (Multi_Map.empty[String, String] /: paths)({ case (tab, path) =>
+ paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) =>
val name = path.expand.implode
tab.insert(Word.lowercase(name), name)
- })
+ }
val collisions =
(for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten
if (collisions.nonEmpty) {
@@ -174,7 +174,7 @@
def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic]
- def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))
+ def +(other: Path): Path = new Path(other.elems.foldRight(elems)(Path.apply_elem))
/* implode */
--- a/src/Pure/General/pretty.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/pretty.scala Fri Mar 05 08:22:34 2021 +0100
@@ -75,7 +75,7 @@
{
val (line, rest) =
Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
- val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
+ val len1 = (line.foldLeft(0.0) { case (l, t) => l + t.length }) max len
(rest: @unchecked) match {
case Break(true, _, ind) :: rest1 =>
body_length(Break(false, indent1 + ind, 0) :: rest1, len1)
--- a/src/Pure/General/scan.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/scan.scala Fri Mar 05 08:22:34 2021 +0100
@@ -323,9 +323,9 @@
/* auxiliary operations */
private def dest(tree: Lexicon.Tree, result: List[String]): List[String] =
- (result /: tree.branches.toList) ((res, entry) =>
- entry match { case (_, (s, tr)) =>
- if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) })
+ tree.branches.toList.foldLeft(result) {
+ case (res, (_, (s, tr))) => if (s.isEmpty) dest(tr, res) else dest(tr, s :: res)
+ }
private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
{
@@ -390,7 +390,8 @@
new Lexicon(extend(rep, 0))
}
- def ++ (elems: IterableOnce[String]): Lexicon = (this /: elems)(_ + _)
+ def ++ (elems: IterableOnce[String]): Lexicon =
+ elems.iterator.foldLeft(this)(_ + _)
def ++ (other: Lexicon): Lexicon =
if (this eq other) this
@@ -478,7 +479,7 @@
def pos: InputPosition = new OffsetPosition(source, offset)
def atEnd: Boolean = !seq.isDefinedAt(offset)
override def drop(n: Int): Paged_Reader = new Paged_Reader(offset + n)
- def close: Unit = buffered_stream.close
+ def close(): Unit = buffered_stream.close()
}
new Paged_Reader(0)
}
--- a/src/Pure/General/sql.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/sql.scala Fri Mar 05 08:22:34 2021 +0100
@@ -253,7 +253,7 @@
def execute(): Boolean = rep.execute()
def execute_query(): Result = new Result(this, rep.executeQuery())
- def close(): Unit = rep.close
+ def close(): Unit = rep.close()
}
@@ -322,7 +322,7 @@
def connection: Connection
- def close(): Unit = connection.close
+ def close(): Unit = connection.close()
def transaction[A](body: => A): A =
{
@@ -483,7 +483,7 @@
val connection = DriverManager.getConnection(url, user, password)
new Database(name, connection, port_forwarding)
}
- catch { case exn: Throwable => port_forwarding.foreach(_.close); throw exn }
+ catch { case exn: Throwable => port_forwarding.foreach(_.close()); throw exn }
}
class Database private[PostgreSQL](
@@ -509,6 +509,6 @@
table.insert_cmd("INSERT",
sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
- override def close(): Unit = { super.close; port_forwarding.foreach(_.close) }
+ override def close(): Unit = { super.close(); port_forwarding.foreach(_.close()) }
}
}
--- a/src/Pure/General/ssh.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/ssh.scala Fri Mar 05 08:22:34 2021 +0100
@@ -141,15 +141,15 @@
val fw =
try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) }
- catch { case exn: Throwable => proxy.close; throw exn }
+ catch { case exn: Throwable => proxy.close(); throw exn }
try {
connect_session(host = fw.local_host, port = fw.local_port,
host_key_permissive = permissive,
nominal_host = host, nominal_user = user, user = user,
- on_close = () => { fw.close; proxy.close })
+ on_close = () => { fw.close(); proxy.close() })
}
- catch { case exn: Throwable => fw.close; proxy.close; throw exn }
+ catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
}
}
}
@@ -259,7 +259,7 @@
progress_stderr: String => Unit = (_: String) => (),
strict: Boolean = true): Process_Result =
{
- stdin.close
+ stdin.close()
def read_lines(stream: InputStream, progress: String => Unit): List[String] =
{
@@ -293,7 +293,7 @@
def terminate(): Unit =
{
- close
+ close()
out_lines.join
err_lines.join
exit_status.join
@@ -303,7 +303,7 @@
try { exit_status.join }
catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
- close
+ close()
if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
Process_Result(rc, out_lines.join, err_lines.join)
--- a/src/Pure/General/symbol.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/symbol.scala Fri Mar 05 08:22:34 2021 +0100
@@ -336,14 +336,14 @@
}
private val symbols: List[(Symbol, Properties.T)] =
- (((List.empty[(Symbol, Properties.T)], Set.empty[Symbol]) /:
- split_lines(symbols_spec).reverse)
- { case (res, No_Decl()) => res
+ split_lines(symbols_spec).reverse.
+ foldLeft((List.empty[(Symbol, Properties.T)], Set.empty[Symbol])) {
+ case (res, No_Decl()) => res
case ((list, known), decl) =>
val (sym, props) = read_decl(decl)
if (known(sym)) (list, known)
else ((sym, props) :: list, known + sym)
- })._1
+ }._1
/* basic properties */
--- a/src/Pure/General/url.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/General/url.scala Fri Mar 05 08:22:34 2021 +0100
@@ -43,7 +43,7 @@
catch { case ERROR(_) => false }
def is_readable(name: String): Boolean =
- try { Url(name).openStream.close; true }
+ try { Url(name).openStream.close(); true }
catch { case ERROR(_) => false }
--- a/src/Pure/Isar/document_structure.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Isar/document_structure.scala Fri Mar 05 08:22:34 2021 +0100
@@ -17,7 +17,7 @@
sealed abstract class Document { def length: Int }
case class Block(name: String, text: String, body: List[Document]) extends Document
- { val length: Int = (0 /: body)(_ + _.length) }
+ { val length: Int = body.foldLeft(0)(_ + _.length) }
case class Atom(length: Int) extends Document
def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =
--- a/src/Pure/Isar/keyword.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Isar/keyword.scala Fri Mar 05 08:22:34 2021 +0100
@@ -160,13 +160,15 @@
val kinds1 =
if (kinds eq other.kinds) kinds
else if (kinds.isEmpty) other.kinds
- else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+ else other.kinds.foldLeft(kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
val load_commands1 =
if (load_commands eq other.load_commands) load_commands
else if (load_commands.isEmpty) other.load_commands
- else
- (load_commands /: other.load_commands) {
- case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+ else {
+ other.load_commands.foldLeft(load_commands) {
+ case (m, e) => if (m.isDefinedAt(e._1)) m else m + e
+ }
+ }
new Keywords(kinds1, load_commands1)
}
@@ -187,7 +189,7 @@
}
def add_keywords(header: Thy_Header.Keywords): Keywords =
- (this /: header) {
+ header.foldLeft(this) {
case (keywords, (name, spec)) =>
if (spec.kind.isEmpty)
keywords + Symbol.decode(name) + Symbol.encode(name)
@@ -217,13 +219,12 @@
/* lexicons */
private def make_lexicon(is_minor: Boolean): Scan.Lexicon =
- (Scan.Lexicon.empty /: kinds)(
- {
- case (lex, (name, kind)) =>
- if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor)
- lex + name
- else lex
- })
+ kinds.foldLeft(Scan.Lexicon.empty) {
+ case (lex, (name, kind)) =>
+ if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor)
+ lex + name
+ else lex
+ }
lazy val minor: Scan.Lexicon = make_lexicon(true)
lazy val major: Scan.Lexicon = make_lexicon(false)
--- a/src/Pure/Isar/line_structure.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Isar/line_structure.scala Fri Mar 05 08:22:34 2021 +0100
@@ -45,7 +45,7 @@
else span_depth
val (span_depth1, after_span_depth1, element_depth1) =
- ((span_depth, after_span_depth, element_depth) /: tokens) {
+ tokens.foldLeft((span_depth, after_span_depth, element_depth)) {
case (depths @ (x, y, z), tok) =>
if (tok.is_begin) (z + 2, z + 1, z + 1)
else if (tok.is_end) (z + 1, z - 1, z - 1)
--- a/src/Pure/Isar/outer_syntax.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Fri Mar 05 08:22:34 2021 +0100
@@ -16,7 +16,7 @@
val empty: Outer_Syntax = new Outer_Syntax()
- def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
+ def merge(syns: List[Outer_Syntax]): Outer_Syntax = syns.foldLeft(empty)(_ ++ _)
/* string literals */
@@ -61,7 +61,7 @@
keywords + (name, kind, load_command), rev_abbrevs, language_context, has_tokens = true)
def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
- (this /: keywords) {
+ keywords.foldLeft(this) {
case (syntax, (name, spec)) =>
syntax +
(Symbol.decode(name), spec.kind, spec.load_command) +
@@ -177,8 +177,9 @@
case Some(cmd) =>
val name = cmd.source
val offset =
- (0 /: content.takeWhile(_ != cmd)) {
- case (i, tok) => i + Symbol.length(tok.source) }
+ content.takeWhile(_ != cmd).foldLeft(0) {
+ case (i, tok) => i + Symbol.length(tok.source)
+ }
val end_offset = offset + Symbol.length(name)
val range = Text.Range(offset, end_offset) + 1
Command_Span.Command_Span(name, Position.Range(range))
@@ -188,8 +189,8 @@
def flush(): Unit =
{
- if (content.nonEmpty) { ship(content.toList); content.clear }
- if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear }
+ if (content.nonEmpty) { ship(content.toList); content.clear() }
+ if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear() }
}
for (tok <- toks) {
@@ -198,7 +199,7 @@
tok.is_command &&
(!content.exists(keywords.is_before_command) || content.exists(_.is_command)))
{ flush(); content += tok }
- else { content ++= ignored; ignored.clear; content += tok }
+ else { content ++= ignored; ignored.clear(); content += tok }
}
flush()
--- a/src/Pure/ML/ml_console.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/ML/ml_console.scala Fri Mar 05 08:22:34 2021 +0100
@@ -74,7 +74,7 @@
else Some(Sessions.base_info(
options, logic, dirs = dirs, include_sessions = include_sessions).check.base))
- POSIX_Interrupt.handler { process.interrupt } {
+ POSIX_Interrupt.handler { process.interrupt() } {
new TTY_Loop(process.stdin, process.stdout).join
val rc = process.join
if (rc != 0) sys.exit(rc)
--- a/src/Pure/ML/ml_statistics.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala Fri Mar 05 08:22:34 2021 +0100
@@ -93,7 +93,7 @@
override def exit(): Unit = synchronized
{
session = null
- monitoring.cancel
+ monitoring.cancel()
}
private def consume(props: Properties.T): Unit = synchronized
@@ -268,7 +268,7 @@
/* content */
def maximum(field: String): Double =
- (0.0 /: content)({ case (m, e) => m max e.get(field) })
+ content.foldLeft(0.0) { case (m, e) => m max e.get(field) }
def average(field: String): Double =
{
--- a/src/Pure/PIDE/command.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/command.scala Fri Mar 05 08:22:34 2021 +0100
@@ -56,8 +56,10 @@
{
type Entry = (Long, XML.Elem)
val empty: Results = new Results(SortedMap.empty)
- def make(args: IterableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
- def merge(args: IterableOnce[Results]): Results = (empty /: args)(_ ++ _)
+ def make(args: IterableOnce[Results.Entry]): Results =
+ args.iterator.foldLeft(empty)(_ + _)
+ def merge(args: IterableOnce[Results]): Results =
+ args.iterator.foldLeft(empty)(_ ++ _)
}
final class Results private(private val rep: SortedMap[Long, XML.Elem])
@@ -74,7 +76,7 @@
def ++ (other: Results): Results =
if (this eq other) this
else if (rep.isEmpty) other
- else (this /: other.iterator)(_ + _)
+ else other.iterator.foldLeft(this)(_ + _)
override def hashCode: Int = rep.hashCode
override def equals(that: Any): Boolean =
@@ -92,7 +94,8 @@
{
type Entry = (Long, Export.Entry)
val empty: Exports = new Exports(SortedMap.empty)
- def merge(args: IterableOnce[Exports]): Exports = (empty /: args)(_ ++ _)
+ def merge(args: IterableOnce[Exports]): Exports =
+ args.iterator.foldLeft(empty)(_ ++ _)
}
final class Exports private(private val rep: SortedMap[Long, Export.Entry])
@@ -107,7 +110,7 @@
def ++ (other: Exports): Exports =
if (this eq other) this
else if (rep.isEmpty) other
- else (this /: other.iterator)(_ + _)
+ else other.iterator.foldLeft(this)(_ + _)
override def hashCode: Int = rep.hashCode
override def equals(that: Any): Boolean =
@@ -134,8 +137,10 @@
type Entry = (Markup_Index, Markup_Tree)
val empty: Markups = new Markups(Map.empty)
def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
- def make(args: IterableOnce[Entry]): Markups = (empty /: args)(_ + _)
- def merge(args: IterableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
+ def make(args: IterableOnce[Entry]): Markups =
+ args.iterator.foldLeft(empty)(_ + _)
+ def merge(args: IterableOnce[Markups]): Markups =
+ args.iterator.foldLeft(empty)(_ ++ _)
}
final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
@@ -157,7 +162,7 @@
def ++ (other: Markups): Markups =
if (this eq other) this
else if (rep.isEmpty) other
- else (this /: other.rep.iterator)(_ + _)
+ else other.rep.iterator.foldLeft(this)(_ + _)
def redirection_iterator: Iterator[Document_ID.Generic] =
for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
@@ -295,21 +300,23 @@
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
if (command.span.is_theory) this
else {
- (this /: msgs)((state, msg) =>
- msg match {
- case elem @ XML.Elem(markup, Nil) =>
- state.
- add_status(markup).
- add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
- case _ =>
- Output.warning("Ignored status message: " + msg)
- state
- })
+ msgs.foldLeft(this) {
+ case (state, msg) =>
+ msg match {
+ case elem @ XML.Elem(markup, Nil) =>
+ state.
+ add_status(markup).
+ add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
+ case _ =>
+ Output.warning("Ignored status message: " + msg)
+ state
+ }
+ }
}
case XML.Elem(Markup(Markup.REPORT, atts0), msgs) =>
- (this /: msgs)((state, msg) =>
- {
+ msgs.foldLeft(this) {
+ case (state, msg) =>
def bad(): Unit = Output.warning("Ignored report message: " + msg)
msg match {
@@ -342,7 +349,7 @@
}
case _ => bad(); state
}
- })
+ }
case XML.Elem(Markup(name, props), body) =>
props match {
@@ -512,7 +519,7 @@
val init_results: Command.Results,
val init_markups: Command.Markups)
{
- override def toString: String = id + "/" + span.kind.toString
+ override def toString: String = id.toString + "/" + span.kind.toString
/* classification */
@@ -562,7 +569,7 @@
val core_range: Text.Range =
Text.Range(0,
- (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
+ span.content.reverse.iterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length))
def source(range: Text.Range): String = range.substring(source)
--- a/src/Pure/PIDE/command_span.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/command_span.scala Fri Mar 05 08:22:34 2021 +0100
@@ -74,7 +74,7 @@
def keyword_pos(start: Token.Pos): Token.Pos =
kind match {
case _: Command_Span =>
- (start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_))
+ content.iterator.takeWhile(tok => !tok.is_command).foldLeft(start)(_.advance(_))
case _ => start
}
@@ -89,7 +89,7 @@
def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content))
- def length: Int = (0 /: content)(_ + _.source.length)
+ def length: Int = content.foldLeft(0)(_ + _.source.length)
def compact_source: (String, Span) =
{
--- a/src/Pure/PIDE/document.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/document.scala Fri Mar 05 08:22:34 2021 +0100
@@ -246,7 +246,7 @@
var p = pos
for (command <- commands) yield {
val start = p
- p = (p /: command.span.content)(_.advance(_))
+ p = command.span.content.foldLeft(p)(_.advance(_))
(command, start)
}
}
@@ -385,7 +385,7 @@
def purge_suppressed: Option[Nodes] =
graph.keys_iterator.filter(is_suppressed).toList match {
case Nil => None
- case del => Some(new Nodes((graph /: del)(_.del_node(_))))
+ case del => Some(new Nodes(del.foldLeft(graph)(_.del_node(_))))
}
def + (entry: (Node.Name, Node)): Nodes =
@@ -393,9 +393,12 @@
val (name, node) = entry
val imports = node.header.imports
val graph1 =
- (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
- val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
- val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
+ imports.foldLeft(graph.default_node(name, Node.empty)) {
+ case (g, p) => g.default_node(p, Node.empty)
+ }
+ val graph2 =
+ graph1.imm_preds(name).foldLeft(graph1) { case (g, dep) => g.del_edge(dep, name) }
+ val graph3 = imports.foldLeft(graph2) { case (g, dep) => g.add_edge(dep, name) }
new Nodes(graph3.map_node(name, _ => node))
}
@@ -449,8 +452,8 @@
def purge_suppressed(
versions: Map[Document_ID.Version, Version]): Map[Document_ID.Version, Version] =
{
- (versions /:
- (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)))(_ + _)
+ (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)).
+ foldLeft(versions)(_ + _)
}
}
@@ -567,9 +570,9 @@
private lazy val reverse_edits = edits.reverse
def convert(offset: Text.Offset): Text.Offset =
- (offset /: edits)((i, edit) => edit.convert(i))
+ edits.foldLeft(offset) { case (i, edit) => edit.convert(i) }
def revert(offset: Text.Offset): Text.Offset =
- (offset /: reverse_edits)((i, edit) => edit.revert(i))
+ reverse_edits.foldLeft(offset) { case (i, edit) => edit.revert(i) }
def convert(range: Text.Range): Text.Range = range.map(convert)
def revert(range: Text.Range): Text.Range = range.map(revert)
@@ -683,7 +686,7 @@
node.commands.iterator.takeWhile(_ != command).map(_.source) ++
(if (offset == 0) Iterator.empty
else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
- val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+ val pos = sources_iterator.foldLeft(Line.Position.zero)(_.advance(_))
Line.Node_Position(name, pos)
}
@@ -842,7 +845,7 @@
{
require(!is_finished, "assignment already finished")
val command_execs1 =
- (command_execs /: update) {
+ update.foldLeft(command_execs) {
case (res, (command_id, exec_ids)) =>
if (exec_ids.isEmpty) res - command_id
else res + (command_id -> exec_ids)
@@ -928,8 +931,10 @@
}
private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
- (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
- graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
+ st.markups.redirection_iterator.foldLeft(commands_redirection) {
+ case (graph, id) =>
+ graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id)
+ }
def accumulate(id: Document_ID.Generic, message: XML.Elem, cache: XML.Cache)
: (Command.State, State) =
@@ -1022,7 +1027,7 @@
if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
val (changed_commands, new_execs) =
- ((Nil: List[Command], execs) /: update) {
+ update.foldLeft((List.empty[Command], execs)) {
case ((commands1, execs1), (command_id, exec)) =>
val st = the_static_state(command_id)
val command = st.command
@@ -1250,10 +1255,10 @@
} yield edits
val edits =
- (pending_edits /: rev_pending_changes)({
+ rev_pending_changes.foldLeft(pending_edits) {
case (edits, Node.Edits(es)) => es ::: edits
case (edits, _) => edits
- })
+ }
new Snapshot(this, version, node_name, edits, snippet_command)
}
--- a/src/Pure/PIDE/document_status.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/document_status.scala Fri Mar 05 08:22:34 2021 +0100
@@ -60,7 +60,7 @@
def merge(status_iterator: Iterator[Command_Status]): Command_Status =
if (status_iterator.hasNext) {
val status0 = status_iterator.next()
- (status0 /: status_iterator)(_ + _)
+ status_iterator.foldLeft(status0)(_ + _)
}
else empty
}
@@ -198,10 +198,10 @@
st <- state.command_states(version, command)
} {
val command_timing =
- (0.0 /: st.status)({
+ st.status.foldLeft(0.0) {
case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
case (timing, _) => timing
- })
+ }
total += command_timing
if (command_timing > 0.0 && command_timing >= threshold) {
command_timings += (command -> command_timing)
--- a/src/Pure/PIDE/headless.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/headless.scala Fri Mar 05 08:22:34 2021 +0100
@@ -154,7 +154,8 @@
if (add.isEmpty) front
else {
val preds = add.map(dep_graph.imm_preds)
- val base1 = (preds.head /: preds.tail)(_ ++ _).toList.filter(already_committed.keySet)
+ val base1 =
+ preds.tail.foldLeft(preds.head)(_ ++ _).toList.filter(already_committed.keySet)
frontier(base1, front ++ add)
}
}
@@ -182,21 +183,21 @@
commit match {
case None => already_committed
case Some(commit_fn) =>
- (already_committed /: dep_graph.topological_order)(
- { case (committed, name) =>
- def parents_committed: Boolean =
- version.nodes(name).header.imports.forall(parent =>
- loaded_theory(parent) || committed.isDefinedAt(parent))
- if (!committed.isDefinedAt(name) && parents_committed &&
- state.node_consolidated(version, name))
- {
- val snapshot = stable_snapshot(state, version, name)
- val status = Document_Status.Node_Status.make(state, version, name)
- commit_fn(snapshot, status)
- committed + (name -> status)
- }
- else committed
- })
+ dep_graph.topological_order.foldLeft(already_committed) {
+ case (committed, name) =>
+ def parents_committed: Boolean =
+ version.nodes(name).header.imports.forall(parent =>
+ loaded_theory(parent) || committed.isDefinedAt(parent))
+ if (!committed.isDefinedAt(name) && parents_committed &&
+ state.node_consolidated(version, name))
+ {
+ val snapshot = stable_snapshot(state, version, name)
+ val status = Document_Status.Node_Status.make(state, version, name)
+ commit_fn(snapshot, status)
+ committed + (name -> status)
+ }
+ else committed
+ }
}
def finished_theory(name: Document.Node.Name): Boolean =
@@ -336,7 +337,7 @@
domain = Some(domain), trim = changed.assignment)
if (nodes_status_delay >= Time.zero && nodes_status_changed) {
- delay_nodes_status.invoke
+ delay_nodes_status.invoke()
}
val theory_progress =
@@ -356,8 +357,8 @@
if (commit.isDefined && commit_cleanup_delay > Time.zero) {
if (use_theories_state.value.finished_result)
- delay_commit_clean.revoke
- else delay_commit_clean.invoke
+ delay_commit_clean.revoke()
+ else delay_commit_clean.invoke()
}
}
}
@@ -367,7 +368,7 @@
session.commands_changed += consumer
check_state()
use_theories_state.guarded_access(_.join_result)
- check_progress.cancel
+ check_progress.cancel()
}
finally {
session.commands_changed -= consumer
@@ -472,8 +473,8 @@
case None => Some(name -> new_blob)
}
})
- val blobs1 = (blobs /: new_blobs)(_ + _)
- val blobs2 = (blobs /: new_blobs)({ case (map, (a, b)) => map + (a -> b.unchanged) })
+ val blobs1 = new_blobs.foldLeft(blobs)(_ + _)
+ val blobs2 = new_blobs.foldLeft(blobs) { case (map, (a, b)) => map + (a -> b.unchanged) }
(Document.Blobs(blobs1), copy(blobs = blobs2))
}
@@ -501,19 +502,20 @@
def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
def insert_required(id: UUID.T, names: List[Document.Node.Name]): State =
- copy(required = (required /: names)(_.insert(_, id)))
+ copy(required = names.foldLeft(required)(_.insert(_, id)))
def remove_required(id: UUID.T, names: List[Document.Node.Name]): State =
- copy(required = (required /: names)(_.remove(_, id)))
+ copy(required = names.foldLeft(required)(_.remove(_, id)))
def update_theories(update: List[(Document.Node.Name, Theory)]): State =
copy(theories =
- (theories /: update)({ case (thys, (name, thy)) =>
- thys.get(name) match {
- case Some(thy1) if thy1 == thy => thys
- case _ => thys + (name -> thy)
- }
- }))
+ update.foldLeft(theories) {
+ case (thys, (name, thy)) =>
+ thys.get(name) match {
+ case Some(thy1) if thy1 == thy => thys
+ case _ => thys + (name -> thy)
+ }
+ })
def remove_theories(remove: List[Document.Node.Name]): State =
{
@@ -573,7 +575,7 @@
progress.echo("Starting session " + session_base_info.session + " ...")
Isabelle_Process(session, options, session_base_info.sessions_structure, store,
- logic = session_base_info.session, modes = print_mode).await_startup
+ logic = session_base_info.session, modes = print_mode).await_startup()
session
}
--- a/src/Pure/PIDE/line.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/line.scala Fri Mar 05 08:22:34 2021 +0100
@@ -118,7 +118,7 @@
private def length(lines: List[Line]): Int =
if (lines.isEmpty) 0
- else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
+ else (lines.foldLeft(0) { case (n, line) => n + line.text.length + 1 }) - 1
def text(lines: List[Line]): String = lines.mkString("", "\n", "")
}
@@ -169,7 +169,7 @@
if (0 <= l && l < n) {
if (0 <= c && c <= lines(l).text.length) {
val line_offset =
- (0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 }
+ lines.iterator.take(l).foldLeft(0) { case (n, line) => n + line.text.length + 1 }
Some(line_offset + c)
}
else None
--- a/src/Pure/PIDE/markup.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/markup.scala Fri Mar 05 08:22:34 2021 +0100
@@ -733,7 +733,7 @@
def update_properties(more_props: Properties.T): Markup =
if (more_props.isEmpty) this
- else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
+ else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) })
def + (entry: Properties.Entry): Markup =
Markup(name, Properties.put(properties, entry))
--- a/src/Pure/PIDE/markup_tree.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Fri Mar 05 08:22:34 2021 +0100
@@ -20,16 +20,16 @@
val empty: Markup_Tree = new Markup_Tree(Branches.empty)
def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree =
- (empty /: trees)(_.merge(_, range, elements))
+ trees.foldLeft(empty)(_.merge(_, range, elements))
def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
trees match {
case Nil => empty
case head :: tail =>
new Markup_Tree(
- (head.branches /: tail) {
+ tail.foldLeft(head.branches) {
case (branches, tree) =>
- (branches /: tree.branches) {
+ tree.branches.foldLeft(branches) {
case (bs, (r, entry)) =>
require(!bs.isDefinedAt(r), "cannot merge markup trees")
bs + (r -> entry)
@@ -93,7 +93,8 @@
(offset + XML.text_length(body), markup_trees)
case (elems, body) =>
- val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)
+ val (end_offset, subtrees) =
+ body.foldLeft((offset, List.empty[Markup_Tree]))(make_trees)
if (offset == end_offset) acc
else {
val range = Text.Range(offset, end_offset)
@@ -104,7 +105,7 @@
}
def from_XML(body: XML.Body): Markup_Tree =
- merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2)
+ merge_disjoint(body.foldLeft((0, List.empty[Markup_Tree]))(make_trees)._2)
}
@@ -163,13 +164,15 @@
def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree =
{
def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
- (tree1 /: tree2.branches)(
- { case (tree, (range, entry)) =>
- if (!range.overlaps(root_range)) tree
- else
- (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
- { case (t, elem) => t + Text.Info(range, elem) })
- })
+ tree2.branches.foldLeft(tree1) {
+ case (tree, (range, entry)) =>
+ if (!range.overlaps(root_range)) tree
+ else {
+ entry.filter_markup(elements).foldLeft(merge_trees(tree, entry.subtree)) {
+ case (t, elem) => t + Text.Info(range, elem)
+ }
+ }
+ }
if (this eq other) this
else {
@@ -236,7 +239,7 @@
else List(XML.Text(text.subSequence(start, stop).toString))
def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
- (body /: rev_markups) {
+ rev_markups.foldLeft(body) {
case (b, elem) =>
if (!elements(elem.name)) b
else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
--- a/src/Pure/PIDE/protocol_handlers.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/protocol_handlers.scala Fri Mar 05 08:22:34 2021 +0100
@@ -74,8 +74,9 @@
private val state = Synchronized(Protocol_Handlers.State(session))
def prover_options(options: Options): Options =
- (options /: state.value.handlers)(
- { case (opts, (_, handler)) => handler.prover_options(opts) })
+ state.value.handlers.foldLeft(options) {
+ case (opts, (_, handler)) => handler.prover_options(opts)
+ }
def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler))
--- a/src/Pure/PIDE/prover.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/prover.scala Fri Mar 05 08:22:34 2021 +0100
@@ -106,7 +106,7 @@
private def terminate_process(): Unit =
{
- try { process.terminate }
+ try { process.terminate() }
catch {
case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
}
@@ -184,7 +184,7 @@
private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
- private def command_input_close(): Unit = command_input.foreach(_.shutdown)
+ private def command_input_close(): Unit = command_input.foreach(_.shutdown())
private def command_input_init(raw_stream: OutputStream): Unit =
{
@@ -204,7 +204,7 @@
}
catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
},
- finish = { case () => stream.close; system_output(name + " terminated") }
+ finish = { case () => stream.close(); system_output(name + " terminated") }
)
)
}
@@ -233,10 +233,10 @@
}
if (result.nonEmpty) {
output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
- result.clear
+ result.clear()
}
else {
- reader.close
+ reader.close()
finished = true
}
//}}}
@@ -333,7 +333,7 @@
case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
}
- stream.close
+ stream.close()
system_output(name + " terminated")
}
@@ -349,7 +349,7 @@
command_input match {
case Some(thread) if thread.is_active =>
if (trace) {
- val payload = (0 /: args)({ case (n, b) => n + b.length })
+ val payload = args.foldLeft(0) { case (n, b) => n + b.length }
Output.writeln(
"protocol_command " + name + ", args = " + args.length + ", payload = " + payload)
}
--- a/src/Pure/PIDE/rendering.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/rendering.scala Fri Mar 05 08:22:34 2021 +0100
@@ -177,7 +177,7 @@
def apply(ids: Set[Long]): Focus = new Focus(ids)
val empty: Focus = apply(Set.empty)
def make(args: List[Text.Info[Focus]]): Focus =
- (empty /: args)({ case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 })
+ args.foldLeft(empty) { case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 }
val full: Focus =
new Focus(Set.empty)
@@ -195,7 +195,7 @@
def ++ (other: Focus): Focus =
if (this eq other) this
else if (rep.isEmpty) other
- else (this /: other.rep.iterator)(_ + _)
+ else other.rep.iterator.foldLeft(this)(_ + _)
override def toString: String = rep.mkString("Focus(", ",", ")")
}
@@ -709,7 +709,7 @@
else {
val r = Text.Range(results.head.range.start, results.last.range.stop)
val all_tips =
- (SortedMap.empty[Long, XML.Tree] /: results.flatMap(_.messages))(_ + _)
+ results.flatMap(_.messages).foldLeft(SortedMap.empty[Long, XML.Tree])(_ + _)
.iterator.map(_._2).toList :::
results.flatMap(res => res.infos(true)) :::
results.flatMap(res => res.infos(false)).lastOption.toList
--- a/src/Pure/PIDE/resources.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Mar 05 08:22:34 2021 +0100
@@ -291,11 +291,12 @@
def session_dependencies(info: Sessions.Info, progress: Progress = new Progress)
: Dependencies[Options] =
{
- (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) =>
- dependencies.require_thys(options,
- for { (thy, pos) <- thys } yield (import_name(info, thy), pos),
- progress = progress)
- })
+ info.theories.foldLeft(Dependencies.empty[Options]) {
+ case (dependencies, (options, thys)) =>
+ dependencies.require_thys(options,
+ for { (thy, pos) <- thys } yield (import_name(info, thy), pos),
+ progress = progress)
+ }
}
object Dependencies
@@ -361,7 +362,7 @@
thys: List[(Document.Node.Name, Position.T)],
progress: Progress = new Progress,
initiators: List[Document.Node.Name] = Nil): Dependencies[A] =
- (this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))
+ thys.foldLeft(this)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))
def entries: List[Document.Node.Entry] = rev_entries.reverse
@@ -392,19 +393,20 @@
}
lazy val loaded_theories: Graph[String, Outer_Syntax] =
- (session_base.loaded_theories /: entries)({ case (graph, entry) =>
- val name = entry.name.theory
- val imports = entry.header.imports.map(_.theory)
-
- val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
- val graph2 = (graph1 /: imports)(_.add_edge(_, name))
+ entries.foldLeft(session_base.loaded_theories) {
+ case (graph, entry) =>
+ val name = entry.name.theory
+ val imports = entry.header.imports.map(_.theory)
- val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
- val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node)
- val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
+ val graph1 = (name :: imports).foldLeft(graph)(_.default_node(_, Outer_Syntax.empty))
+ val graph2 = imports.foldLeft(graph1)(_.add_edge(_, name))
- graph2.map_node(name, _ => syntax)
- })
+ val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
+ val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node)
+ val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
+
+ graph2.map_node(name, _ => syntax)
+ }
def get_syntax(name: Document.Node.Name): Outer_Syntax =
loaded_theories.get_node(name.theory)
--- a/src/Pure/PIDE/session.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/session.scala Fri Mar 05 08:22:34 2021 +0100
@@ -624,7 +624,7 @@
delay_prune.revoke()
if (prover.defined) {
global_state.change(_ => Document.State.init)
- prover.get.terminate
+ prover.get.terminate()
}
case Get_State(promise) =>
--- a/src/Pure/PIDE/xml.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/PIDE/xml.scala Fri Mar 05 08:22:34 2021 +0100
@@ -101,11 +101,11 @@
{
def traverse(x: A, t: Tree): A =
t match {
- case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
- case XML.Elem(_, ts) => (x /: ts)(traverse)
+ case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse)
+ case XML.Elem(_, ts) => ts.foldLeft(x)(traverse)
case XML.Text(s) => op(x, s)
}
- (a /: body)(traverse)
+ body.foldLeft(a)(traverse)
}
def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
--- a/src/Pure/ROOT.ML Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/ROOT.ML Fri Mar 05 08:22:34 2021 +0100
@@ -355,4 +355,3 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML"
-
--- a/src/Pure/System/bash.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/bash.scala Fri Mar 05 08:22:34 2021 +0100
@@ -108,7 +108,7 @@
def terminate(): Unit = Isabelle_Thread.try_uninterruptible
{
kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL")
- proc.destroy
+ proc.destroy()
do_cleanup()
}
@@ -173,7 +173,7 @@
watchdog: Option[Watchdog] = None,
strict: Boolean = true): Process_Result =
{
- stdin.close
+ stdin.close()
val out_lines =
Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) }
@@ -195,7 +195,7 @@
try { join }
catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
- watchdog_thread.foreach(_.cancel)
+ watchdog_thread.foreach(_.cancel())
if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
--- a/src/Pure/System/getopts.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/getopts.scala Fri Mar 05 08:22:34 2021 +0100
@@ -15,7 +15,7 @@
def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
{
val options =
- (Map.empty[Char, (Boolean, String => Unit)] /: option_specs) {
+ option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) {
case (m, (s, f)) =>
val (a, entry) =
if (s.size == 1) (s(0), (false, f))
--- a/src/Pure/System/isabelle_charset.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/isabelle_charset.scala Fri Mar 05 08:22:34 2021 +0100
@@ -12,8 +12,6 @@
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
import java.nio.charset.spi.CharsetProvider
-import scala.collection.JavaConverters
-
object Isabelle_Charset
{
@@ -47,6 +45,6 @@
{
// FIXME inactive
// Iterator(Isabelle_Charset.charset)
- JavaConverters.asJavaIterator(Iterator())
+ java.util.List.of[Charset]().listIterator()
}
}
--- a/src/Pure/System/isabelle_process.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/isabelle_process.scala Fri Mar 05 08:22:34 2021 +0100
@@ -37,7 +37,7 @@
modes = modes, cwd = cwd, env = env)
}
catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
- process.stdin.close
+ process.stdin.close()
new Isabelle_Process(session, channel, process)
}
@@ -77,5 +77,5 @@
result
}
- def terminate: Unit = process.terminate
+ def terminate(): Unit = process.terminate()
}
--- a/src/Pure/System/isabelle_system.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala Fri Mar 05 08:22:34 2021 +0100
@@ -421,7 +421,7 @@
proc.command(command_line:_*) // fragile on Windows
if (cwd != null) proc.directory(cwd)
if (env != null) {
- proc.environment.clear
+ proc.environment.clear()
for ((x, y) <- env) proc.environment.put(x, y)
}
proc.redirectErrorStream(redirect)
@@ -430,15 +430,15 @@
def process_output(proc: Process): (String, Int) =
{
- proc.getOutputStream.close
+ proc.getOutputStream.close()
val output = File.read_stream(proc.getInputStream)
val rc =
try { proc.waitFor }
finally {
- proc.getInputStream.close
- proc.getErrorStream.close
- proc.destroy
+ proc.getInputStream.close()
+ proc.getErrorStream.close()
+ proc.destroy()
Exn.Interrupt.dispose()
}
(output, rc)
--- a/src/Pure/System/isabelle_tool.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/isabelle_tool.scala Fri Mar 05 08:22:34 2021 +0100
@@ -29,11 +29,14 @@
val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
try {
- val symbol = tool_box.parse(source) match {
- case tree: universe.ModuleDef => tool_box.define(tree)
- case _ => err("Source does not describe a module (Scala object)")
- }
- tool_box.compile(universe.Ident(symbol))() match {
+ val tree = tool_box.parse(source)
+ val module =
+ try { tree.asInstanceOf[universe.ModuleDef] }
+ catch {
+ case _: java.lang.ClassCastException =>
+ err("Source does not describe a module (Scala object)")
+ }
+ tool_box.compile(universe.Ident(tool_box.define(module)))() match {
case body: Body => body
case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
}
@@ -157,7 +160,7 @@
Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
-Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage
+Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage()
case tool_name :: tool_args =>
find_external(tool_name) orElse find_internal(tool_name) match {
case Some(tool) => tool(tool_args)
--- a/src/Pure/System/options.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/options.scala Fri Mar 05 08:22:34 2021 +0100
@@ -119,7 +119,7 @@
case Success(result, _) => result
case bad => error(bad.toString)
}
- try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } }
+ try { ops.foldLeft(options.set_section("")) { case (opts, op) => op(opts) } }
catch { case ERROR(msg) => error(msg + Position.here(Position.File(file_name))) }
}
@@ -137,7 +137,7 @@
dir <- Isabelle_System.components()
file = dir + OPTIONS if file.is_file
} { options = Parser.parse_file(options, file.implode, File.read(file)) }
- (Options.Parser.parse_prefs(options, prefs) /: opts)(_ + _)
+ opts.foldLeft(Options.Parser.parse_prefs(options, prefs))(_ + _)
}
@@ -181,9 +181,9 @@
val options0 = Options.init()
val options1 =
if (build_options)
- (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
+ Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _)
else options0
- (options1 /: more_options)(_ + _)
+ more_options.foldLeft(options1)(_ + _)
}
if (get_option != "")
@@ -363,7 +363,7 @@
}
def ++ (specs: List[Options.Spec]): Options =
- (this /: specs)({ case (x, (y, z)) => x + (y, z) })
+ specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) }
/* sections */
--- a/src/Pure/System/posix_interrupt.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/posix_interrupt.scala Fri Mar 05 08:22:34 2021 +0100
@@ -23,7 +23,7 @@
def exception[A](e: => A): A =
{
val thread = Thread.currentThread
- handler { thread.interrupt } { e }
+ handler { thread.interrupt() } { e }
}
}
--- a/src/Pure/System/progress.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/progress.scala Fri Mar 05 08:22:34 2021 +0100
@@ -37,14 +37,14 @@
Timing.timeit(message, enabled, echo)(e)
@volatile protected var is_stopped = false
- def stop: Unit = { is_stopped = true }
+ def stop(): Unit = { is_stopped = true }
def stopped: Boolean =
{
- if (Thread.interrupted) is_stopped = true
+ if (Thread.interrupted()) is_stopped = true
is_stopped
}
- def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop } { e }
+ def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop() } { e }
def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt()
override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
--- a/src/Pure/System/scala.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/scala.scala Fri Mar 05 08:22:34 2021 +0100
@@ -114,7 +114,7 @@
if (interpret) interp.interpret(source) == Results.Success
else (new interp.ReadEvalPrint).compile(source)
}
- out.close
+ out.close()
val Error = """(?s)^\S* error: (.*)$""".r
val errors =
@@ -195,7 +195,7 @@
private def cancel(id: String, future: Future[Unit]): Unit =
{
- future.cancel
+ future.cancel()
result(id, Scala.Tag.INTERRUPT, "")
}
--- a/src/Pure/System/system_channel.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/system_channel.scala Fri Mar 05 08:22:34 2021 +0100
@@ -25,7 +25,7 @@
override def toString: String = address
- def shutdown(): Unit = server.close
+ def shutdown(): Unit = server.close()
def rendezvous(): (OutputStream, InputStream) =
{
@@ -36,8 +36,8 @@
if (Byte_Message.read_line(in_stream).map(_.text) == Some(password)) (out_stream, in_stream)
else {
- out_stream.close
- in_stream.close
+ out_stream.close()
+ in_stream.close()
error("Failed to connect system channel: bad password")
}
}
--- a/src/Pure/System/tty_loop.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/System/tty_loop.scala Fri Mar 05 08:22:34 2021 +0100
@@ -30,7 +30,7 @@
if (result.nonEmpty) {
System.out.print(result.toString)
System.out.flush()
- result.clear
+ result.clear()
}
else {
reader.close()
@@ -64,5 +64,5 @@
def join: Unit = { console_output.join; console_input.join }
- def cancel: Unit = console_input.cancel
+ def cancel(): Unit = console_input.cancel()
}
--- a/src/Pure/Thy/bibtex.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/bibtex.scala Fri Mar 05 08:22:34 2021 +0100
@@ -389,7 +389,9 @@
def heading_length: Int =
if (name == "") 1
- else (0 /: tokens.takeWhile(tok => !tok.is_open)){ case (n, tok) => n + tok.source.length }
+ else {
+ tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length }
+ }
def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
--- a/src/Pure/Thy/export_theory.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala Fri Mar 05 08:22:34 2021 +0100
@@ -48,12 +48,16 @@
}))
val graph0 =
- (Graph.string[Option[Theory]] /: thys) {
- case (g, thy) => g.default_node(thy.name, Some(thy)) }
+ thys.foldLeft(Graph.string[Option[Theory]]) {
+ case (g, thy) => g.default_node(thy.name, Some(thy))
+ }
val graph1 =
- (graph0 /: thys) { case (g0, thy) =>
- (g0 /: thy.parents) { case (g1, parent) =>
- g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) } }
+ thys.foldLeft(graph0) {
+ case (g0, thy) =>
+ thy.parents.foldLeft(g0) {
+ case (g1, parent) => g1.default_node(parent, None).add_edge_acyclic(parent, thy.name)
+ }
+ }
Session(session_name, graph1)
}
--- a/src/Pure/Thy/file_format.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/file_format.scala Fri Mar 05 08:22:34 2021 +0100
@@ -39,15 +39,15 @@
agents.mkString("File_Format.Session(", ", ", ")")
def prover_options(options: Options): Options =
- (options /: agents)({ case (opts, agent) => agent.prover_options(opts) })
+ agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) }
- def stop_session: Unit = agents.foreach(_.stop)
+ def stop_session: Unit = agents.foreach(_.stop())
}
trait Agent
{
def prover_options(options: Options): Options = options
- def stop: Unit = {}
+ def stop(): Unit = {}
}
object No_Agent extends Agent
--- a/src/Pure/Thy/latex.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/latex.scala Fri Mar 05 08:22:34 2021 +0100
@@ -67,8 +67,8 @@
case None => None
case Some(file) =>
val source_line =
- (0 /: source_lines.iterator.takeWhile({ case (m, _) => m <= l }))(
- { case (_, (_, n)) => n })
+ source_lines.iterator.takeWhile({ case (m, _) => m <= l }).
+ foldLeft(0) { case (_, (_, n)) => n }
if (source_line == 0) None else Some(Position.Line_File(source_line, file))
}
--- a/src/Pure/Thy/sessions.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Mar 05 08:22:34 2021 +0100
@@ -11,7 +11,7 @@
import java.nio.channels.FileChannel
import java.nio.file.StandardOpenOption
-import scala.collection.{SortedSet, SortedMap}
+import scala.collection.immutable.{SortedSet, SortedMap}
import scala.collection.mutable
@@ -156,7 +156,7 @@
}
val session_bases =
- (Map("" -> sessions_structure.bootstrap) /: sessions_structure.imports_topological_order)({
+ sessions_structure.imports_topological_order.foldLeft(Map("" -> sessions_structure.bootstrap)) {
case (session_bases, session_name) =>
progress.expose_interrupt()
@@ -230,22 +230,24 @@
.transitive_reduction_acyclic
val graph0 =
- (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)
- ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
+ required_subgraph.topological_order.foldLeft(Graph_Display.empty_graph) {
+ case (g, session) =>
+ val a = session_node(session)
+ val bs = required_subgraph.imm_preds(session).toList.map(session_node)
+ bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a))
+ }
- (graph0 /: dependencies.entries)(
- { case (g, entry) =>
- val a = node(entry.name)
- val bs = entry.header.imports.map(node).filterNot(_ == a)
- ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
+ dependencies.entries.foldLeft(graph0) {
+ case (g, entry) =>
+ val a = node(entry.name)
+ val bs = entry.header.imports.map(node).filterNot(_ == a)
+ bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a))
+ }
}
val known_theories =
- (deps_base.known_theories /:
- dependencies.entries.iterator.map(entry => entry.name.theory -> entry))(_ + _)
+ dependencies.entries.iterator.map(entry => entry.name.theory -> entry).
+ foldLeft(deps_base.known_theories)(_ + _)
val known_loaded_files = deps_base.known_loaded_files ++ loaded_files
@@ -357,7 +359,7 @@
cat_error(msg, "The error(s) above occurred in session " +
quote(info.name) + Position.here(info.pos))
}
- })
+ }
Deps(sessions_structure, session_bases)
}
@@ -489,14 +491,13 @@
val imports_bases = imports.map(session_bases)
parent_base.copy(
known_theories =
- (parent_base.known_theories /:
- (for {
- base <- imports_bases.iterator
- (_, entry) <- base.known_theories.iterator
- } yield (entry.name.theory -> entry)))(_ + _),
+ (for {
+ base <- imports_bases.iterator
+ (_, entry) <- base.known_theories.iterator
+ } yield (entry.name.theory -> entry)).foldLeft(parent_base.known_theories)(_ + _),
known_loaded_files =
- (parent_base.known_loaded_files /:
- imports_bases.iterator.map(_.known_loaded_files))(_ ++ _))
+ imports_bases.iterator.map(_.known_loaded_files).
+ foldLeft(parent_base.known_loaded_files)(_ ++ _))
}
def dirs: List[Path] = dir :: directories
@@ -661,13 +662,14 @@
cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
}
}
- (graph /: graph.iterator) {
- case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _))
+ graph.iterator.foldLeft(graph) {
+ case (g, (name, (info, _))) =>
+ edges(info).foldLeft(g)(add_edge(info.pos, name, _, _))
}
}
val info_graph =
- (Graph.string[Info] /: infos) {
+ infos.foldLeft(Graph.string[Info]) {
case (graph, info) =>
if (graph.defined(info.name))
error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
@@ -681,12 +683,12 @@
(for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList
val session_directories: Map[JFile, String] =
- (Map.empty[JFile, String] /:
- (for {
- session <- imports_graph.topological_order.iterator
- info = info_graph.get_node(session)
- dir <- info.dirs.iterator
- } yield (info, dir)))({ case (dirs, (info, dir)) =>
+ (for {
+ session <- imports_graph.topological_order.iterator
+ info = info_graph.get_node(session)
+ dir <- info.dirs.iterator
+ } yield (info, dir)).foldLeft(Map.empty[JFile, String]) {
+ case (dirs, (info, dir)) =>
val session = info.name
val canonical_dir = dir.canonical_file
dirs.get(canonical_dir) match {
@@ -697,22 +699,22 @@
"\n vs. session " + quote(session) + Position.here(info.pos))
case None => dirs + (canonical_dir -> session)
}
- })
+ }
val global_theories: Map[String, String] =
- (Thy_Header.bootstrap_global_theories.toMap /:
- (for {
- session <- imports_graph.topological_order.iterator
- info = info_graph.get_node(session)
- thy <- info.global_theories.iterator }
- yield (info, thy)))({ case (global, (info, thy)) =>
+ (for {
+ session <- imports_graph.topological_order.iterator
+ info = info_graph.get_node(session)
+ thy <- info.global_theories.iterator }
+ yield (info, thy)).foldLeft(Thy_Header.bootstrap_global_theories.toMap) {
+ case (global, (info, thy)) =>
val qualifier = info.name
global.get(thy) match {
case Some(qualifier1) if qualifier != qualifier1 =>
error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
case _ => global + (thy -> qualifier)
}
- })
+ }
new Structure(
session_positions, session_directories, global_theories, build_graph, imports_graph)
@@ -739,9 +741,10 @@
yield (File.standard_path(file), session)
lazy val chapters: SortedMap[String, List[Info]] =
- (SortedMap.empty[String, List[Info]] /: build_graph.iterator)(
- { case (chs, (_, (info, _))) =>
- chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) })
+ build_graph.iterator.foldLeft(SortedMap.empty[String, List[Info]]) {
+ case (chs, (_, (info, _))) =>
+ chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil)))
+ }
def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
@@ -1061,13 +1064,14 @@
} yield res
val unique_roots =
- ((Map.empty[JFile, (Boolean, Path)] /: roots) { case (m, (select, path)) =>
- val file = path.canonical_file
- m.get(file) match {
- case None => m + (file -> (select, path))
- case Some((select1, path1)) => m + (file -> (select1 || select, path1))
- }
- }).toList.map(_._2)
+ roots.foldLeft(Map.empty[JFile, (Boolean, Path)]) {
+ case (m, (select, path)) =>
+ val file = path.canonical_file
+ m.get(file) match {
+ case None => m + (file -> (select, path))
+ case Some((select1, path1)) => m + (file -> (select1 || select, path1))
+ }
+ }.toList.map(_._2)
Structure.make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos)
}
@@ -1210,7 +1214,7 @@
{
def cache: XML.Cache = store.cache
- def close: Unit = database_server.foreach(_.close)
+ def close(): Unit = database_server.foreach(_.close())
def output_database[A](session: String)(f: SQL.Database => A): A =
database_server match {
@@ -1346,7 +1350,7 @@
def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] =
{
def check(db: SQL.Database): Option[SQL.Database] =
- if (output || session_info_exists(db)) Some(db) else { db.close; None }
+ if (output || session_info_exists(db)) Some(db) else { db.close(); None }
if (database_server) check(open_database_server())
else if (output) Some(SQLite.open_database(output_database(name)))
@@ -1376,7 +1380,7 @@
init_session_info(db, name)
relevant_db
}
- } finally { db.close }
+ } finally { db.close() }
case None => false
}
}
@@ -1416,16 +1420,16 @@
db.transaction {
db.create_table(Session_Info.table)
db.using_statement(
- Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
+ Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute())
db.create_table(Export.Data.table)
db.using_statement(
- Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute)
+ Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute())
db.create_table(Presentation.Data.table)
db.using_statement(
Presentation.Data.table.delete(
- Presentation.Data.session_name.where_equal(name)))(_.execute)
+ Presentation.Data.session_name.where_equal(name)))(_.execute())
}
}
--- a/src/Pure/Thy/thy_header.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/thy_header.scala Fri Mar 05 08:22:34 2021 +0100
@@ -186,10 +186,10 @@
private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) =
{
val token = Token.Parsers.token(bootstrap_keywords)
- def make_tokens(in: Reader[Char]): Stream[Token] =
+ def make_tokens(in: Reader[Char]): LazyList[Token] =
token(in) match {
case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest)
- case _ => Stream.empty
+ case _ => LazyList.empty
}
val all_tokens = make_tokens(reader)
@@ -223,7 +223,7 @@
val (skip_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
val pos =
if (command) Token.Pos.command
- else (Token.Pos.file(node_name.node) /: skip_tokens)(_ advance _)
+ else skip_tokens.foldLeft(Token.Pos.file(node_name.node))(_ advance _)
Parser.parse_header(tokens, pos).map(Symbol.decode).check(node_name)
}
--- a/src/Pure/Thy/thy_syntax.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Fri Mar 05 08:22:34 2021 +0100
@@ -27,7 +27,7 @@
val visible = new mutable.ListBuffer[Command]
val visible_overlay = new mutable.ListBuffer[Command]
@tailrec
- def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)]): Unit =
+ def check_ranges(ranges: List[Text.Range], commands: LazyList[(Command, Text.Offset)]): Unit =
{
(ranges, commands) match {
case (range :: more_ranges, (command, offset) #:: more_commands) =>
@@ -55,7 +55,7 @@
val commands =
(if (overlays.is_empty) node.command_iterator(perspective.range)
- else node.command_iterator()).toStream
+ else node.command_iterator()).to(LazyList)
check_ranges(perspective.ranges, commands)
(Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
}
@@ -191,7 +191,7 @@
val inserted =
blobs_spans2.map({ case (blobs, span) =>
Command(Document_ID.make(), node_name, blobs, span) })
- (commands /: cmds2)(_ - _).append_after(hook, inserted)
+ cmds2.foldLeft(commands)(_ - _).append_after(hook, inserted)
}
}
@@ -310,12 +310,12 @@
if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
else {
val reparse =
- (syntax_changed /: nodes0.iterator)({
+ nodes0.iterator.foldLeft(syntax_changed) {
case (reparse, (name, node)) =>
if (node.load_commands_changed(doc_blobs) && !reparse.contains(name))
name :: reparse
else reparse
- })
+ }
val reparse_set = reparse.toSet
var nodes = nodes0
@@ -338,7 +338,7 @@
commands, commands.head, commands.last))
else node
val node2 =
- (node1 /: edits)(
+ edits.foldLeft(node1)(
text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
val node3 =
if (reparse_set.contains(name))
--- a/src/Pure/Tools/build.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/build.scala Fri Mar 05 08:22:34 2021 +0100
@@ -8,7 +8,7 @@
package isabelle
-import scala.collection.SortedSet
+import scala.collection.immutable.SortedSet
import scala.annotation.tailrec
@@ -60,7 +60,7 @@
case exn: java.lang.Error => ignore_error(Exn.message(exn))
case _: XML.Error => ignore_error("")
}
- finally { db.close }
+ finally { db.close() }
}
}
@@ -99,16 +99,8 @@
object Ordering extends scala.math.Ordering[String]
{
- def compare_timing(name1: String, name2: String): Int =
- {
- val t1 = session_timing(name1)
- val t2 = session_timing(name2)
- if (t1 == 0.0 || t2 == 0.0) 0
- else t1 compare t2
- }
-
def compare(name1: String, name2: String): Int =
- compare_timing(name2, name1) match {
+ session_timing(name2) compare session_timing(name1) match {
case 0 =>
sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
case 0 => name1 compare name2
@@ -132,16 +124,11 @@
def is_empty: Boolean = graph.is_empty
def - (name: String): Queue =
- new Queue(graph.del_node(name),
- order - name, // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
- command_timings)
+ new Queue(graph.del_node(name), order - name, command_timings)
def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
{
- val it = order.iterator.dropWhile(name =>
- skip(name)
- || !graph.defined(name) // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
- || !graph.is_minimal(name))
+ val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
else None
}
@@ -159,8 +146,8 @@
def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
def info(name: String): Sessions.Info = results(name)._2
val rc: Int =
- (0 /: results.iterator.map(
- { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
+ results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
+ foldLeft(0)(_ max _)
def ok: Boolean = rc == 0
override def toString: String = rc.toString
@@ -303,7 +290,7 @@
}
def sleep(): Unit =
- Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep }
+ Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep }
val numa_nodes = new NUMA.Nodes(numa_shuffling)
@@ -319,7 +306,7 @@
if (pending.is_empty) results
else {
if (progress.stopped) {
- for ((_, (_, job)) <- running) job.terminate
+ for ((_, (_, job)) <- running) job.terminate()
}
running.find({ case (_, (_, job)) => job.is_finished }) match {
@@ -661,7 +648,7 @@
}
val total_timing =
- (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
+ results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
copy(elapsed = elapsed_time)
progress.echo(total_timing.message_resources)
--- a/src/Pure/Tools/build_job.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/build_job.scala Fri Mar 05 08:22:34 2021 +0100
@@ -253,7 +253,7 @@
private val promise: Promise[List[String]] = Future.promise
def result: Exn.Result[List[String]] = promise.join_result
- def cancel: Unit = promise.cancel
+ def cancel(): Unit = promise.cancel()
def apply(errs: List[String]): Unit =
{
try { promise.fulfill(errs) }
@@ -286,7 +286,7 @@
session.init_protocol_handler(new Session.Protocol_Handler
{
- override def exit(): Unit = Build_Session_Errors.cancel
+ override def exit(): Unit = Build_Session_Errors.cancel()
private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
{
@@ -416,8 +416,8 @@
cwd = info.dir.file, env = env)
val build_errors =
- Isabelle_Thread.interrupt_handler(_ => process.terminate) {
- Exn.capture { process.await_startup } match {
+ Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
+ Exn.capture { process.await_startup() } match {
case Exn.Res(_) =>
val resources_yxml = resources.init_session_yxml
val args_yxml =
@@ -434,7 +434,7 @@
}
val process_result =
- Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
+ Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() }
session.stop()
@@ -502,13 +502,13 @@
}
}
- def terminate: Unit = future_result.cancel
+ def terminate(): Unit = future_result.cancel()
def is_finished: Boolean = future_result.is_finished
private val timeout_request: Option[Event_Timer.Request] =
{
if (info.timeout > Time.zero)
- Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
+ Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
else None
}
@@ -519,7 +519,7 @@
val was_timeout =
timeout_request match {
case None => false
- case Some(request) => !request.cancel
+ case Some(request) => !request.cancel()
}
val result2 =
--- a/src/Pure/Tools/dump.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/dump.scala Fri Mar 05 08:22:34 2021 +0100
@@ -105,7 +105,7 @@
"completion_limit=0" +
"editor_tracing_messages=0" +
"editor_presentation"
- (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+ aspects.foldLeft(options1) { case (opts, aspect) => aspect.options.foldLeft(opts)(_ + _) }
}
val sessions_structure: Sessions.Structure =
--- a/src/Pure/Tools/scala_project.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/scala_project.scala Fri Mar 05 08:22:34 2021 +0100
@@ -53,7 +53,7 @@
}
lazy val isabelle_scala_files: Map[String, Path] =
- (Map.empty[String, Path] /: isabelle_files)({
+ isabelle_files.foldLeft(Map.empty[String, Path]) {
case (map, name) =>
if (!name.startsWith("src/Tools/jEdit/") && name.endsWith(".scala")) {
val path = Path.explode("~~/" + name)
@@ -64,7 +64,7 @@
}
}
else map
- })
+ }
val isabelle_dirs: List[(String, Path)] =
List(
--- a/src/Pure/Tools/server.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/server.scala Fri Mar 05 08:22:34 2021 +0100
@@ -74,12 +74,13 @@
}
private lazy val command_table: Map[String, Command] =
- (Map.empty[String, Command] /: Isabelle_System.make_services(classOf[Commands]).flatMap(_.entries))(
- { case (cmds, cmd) =>
+ Isabelle_System.make_services(classOf[Commands]).flatMap(_.entries).
+ foldLeft(Map.empty[String, Command]) {
+ case (cmds, cmd) =>
val name = cmd.command_name
if (cmds.isDefinedAt(name)) error("Duplicate Isabelle server command: " + quote(name))
else cmds + (name -> cmd)
- })
+ }
/* output reply */
@@ -148,9 +149,9 @@
}
}
- def start: Unit = thread
+ def start(): Unit = thread
def join: Unit = thread.join
- def stop: Unit = { socket.close; join }
+ def stop(): Unit = { socket.close(); join }
}
@@ -166,7 +167,7 @@
{
override def toString: String = socket.toString
- def close(): Unit = socket.close
+ def close(): Unit = socket.close()
def set_timeout(t: Time): Unit = socket.setSoTimeout(t.ms.toInt)
@@ -249,11 +250,11 @@
_tasks.change(_ - task)
def cancel_task(id: UUID.T): Unit =
- _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks })
+ _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel()); tasks })
def close(): Unit =
{
- while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) }))
+ while(_tasks.change_result(tasks => { tasks.foreach(_.cancel()); (tasks.nonEmpty, tasks) }))
{ _tasks.value.foreach(_.join) }
}
}
@@ -292,7 +293,7 @@
val ident: JSON.Object.Entry = ("task" -> id.toString)
val progress: Connection_Progress = context.progress(ident)
- def cancel: Unit = progress.stop
+ def cancel(): Unit = progress.stop()
private lazy val thread = Isabelle_Thread.fork(name = "server_task")
{
@@ -303,7 +304,7 @@
val err = json_error(exn)
if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident)
}
- progress.stop
+ progress.stop()
context.remove_task(task)
}
def start: Unit = thread
@@ -350,7 +351,7 @@
connection
}
- def active(): Boolean =
+ def active: Boolean =
try {
using(connection())(connection =>
{
@@ -410,7 +411,7 @@
db.create_table(Data.table)
list(db).filterNot(_.active).foreach(server_info =>
db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
- _.execute))
+ _.execute()))
}
db.transaction {
find(db, name) match {
@@ -421,7 +422,7 @@
val server = new Server(port, log)
val server_info = Info(name, server.port, server.password)
- db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
+ db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute())
db.using_statement(Data.table.insert())(stmt =>
{
stmt.string(1) = server_info.name
@@ -430,7 +431,7 @@
stmt.execute()
})
- server.start
+ server.start()
(server_info, Some(server))
}
}
@@ -533,7 +534,7 @@
def shutdown(): Unit =
{
- server.socket.close
+ server.socket.close()
val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
for ((_, session) <- sessions) {
--- a/src/Pure/Tools/spell_checker.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/Tools/spell_checker.scala Fri Mar 05 08:22:34 2021 +0100
@@ -88,7 +88,7 @@
}
}
- def dictionaries(): List[Dictionary] =
+ def dictionaries: List[Dictionary] =
for {
path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
if path.is_file
--- a/src/Pure/library.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Pure/library.scala Fri Mar 05 08:22:34 2021 +0100
@@ -96,9 +96,11 @@
/* lines */
- def terminate_lines(lines: IterableOnce[String]): String = lines.mkString("", "\n", "\n")
+ def terminate_lines(lines: IterableOnce[String]): String =
+ lines.iterator.mkString("", "\n", "\n")
- def cat_lines(lines: IterableOnce[String]): String = lines.mkString("\n")
+ def cat_lines(lines: IterableOnce[String]): String =
+ lines.iterator.mkString("\n")
def split_lines(str: String): List[String] = space_explode('\n', str)
@@ -126,7 +128,9 @@
/* strings */
- def cat_strings0(strs: IterableOnce[String]): String = strs.mkString("\u0000")
+ def cat_strings0(strs: IterableOnce[String]): String =
+ strs.iterator.mkString("\u0000")
+
def split_strings0(str: String): List[String] = space_explode('\u0000', str)
def make_string(f: StringBuilder => Unit): String =
--- a/src/Tools/Graphview/graph_panel.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Fri Mar 05 08:22:34 2021 +0100
@@ -341,8 +341,8 @@
tooltip = "Use editor font and colors for painting"
}
- private val colorations = new Button { action = Action("Colorations") { color_dialog.open } }
- private val filters = new Button { action = Action("Filters") { mutator_dialog.open } }
+ private val colorations = new Button { action = Action("Colorations") { color_dialog.open() } }
+ private val filters = new Button { action = Action("Filters") { mutator_dialog.open() } }
private val controls =
Wrap_Panel(
--- a/src/Tools/Graphview/layout.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/layout.scala Fri Mar 05 08:22:34 2021 +0100
@@ -108,10 +108,10 @@
}).toList)
val initial_levels: Levels =
- (empty_levels /: initial_graph.topological_order) {
+ initial_graph.topological_order.foldLeft(empty_levels) {
case (levels, vertex) =>
val level =
- 1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) }
+ 1 + initial_graph.imm_preds(vertex).foldLeft(-1) { case (m, v) => m max levels(v) }
levels + (vertex -> level)
}
@@ -121,25 +121,26 @@
val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil)
val (dummy_graph, dummy_levels) =
- ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
- case ((graph, levels), (node1, node2)) =>
- val v1 = Node(node1); val l1 = levels(v1)
- val v2 = Node(node2); val l2 = levels(v2)
- if (l2 - l1 <= 1) (graph, levels)
- else {
- val dummies_levels =
- (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
- yield (Dummy(node1, node2, i), l)).toList
- val dummies = dummies_levels.map(_._1)
+ input_graph.edges_iterator.foldLeft((initial_graph, initial_levels)) {
+ case ((graph, levels), (node1, node2)) =>
+ val v1 = Node(node1); val l1 = levels(v1)
+ val v2 = Node(node2); val l2 = levels(v2)
+ if (l2 - l1 <= 1) (graph, levels)
+ else {
+ val dummies_levels =
+ (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
+ yield (Dummy(node1, node2, i), l)).toList
+ val dummies = dummies_levels.map(_._1)
- val levels1 = (levels /: dummies_levels)(_ + _)
- val graph1 =
- ((graph /: dummies)(_.new_node(_, dummy_info)).del_edge(v1, v2) /:
- (v1 :: dummies ::: List(v2)).sliding(2)) {
- case (g, List(a, b)) => g.add_edge(a, b) }
- (graph1, levels1)
- }
- }
+ val levels1 = dummies_levels.foldLeft(levels)(_ + _)
+ val graph1 =
+ (v1 :: dummies ::: List(v2)).sliding(2).
+ foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) {
+ case (g, List(a, b)) => g.add_edge(a, b)
+ }
+ (graph1, levels1)
+ }
+ }
/* minimize edge crossings and initial coordinates */
@@ -147,25 +148,26 @@
val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels))
val levels_graph: Graph =
- (((dummy_graph, 0.0) /: levels) {
+ levels.foldLeft((dummy_graph, 0.0)) {
case ((graph, y), level) =>
- val num_lines = (0 /: level) { case (n, v) => n max graph.get_node(v).lines.length }
- val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size }
+ val num_lines = level.foldLeft(0) { case (n, v) => n max graph.get_node(v).lines.length }
+ val num_edges = level.foldLeft(0) { case (n, v) => n + graph.imm_succs(v).size }
val y1 = y + metrics.node_height2(num_lines)
val graph1 =
- (((graph, 0.0) /: level) { case ((g, x), v) =>
- val info = g.get_node(v)
- val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
- val x1 = x + info.width + metrics.gap
- (g1, x1)
- })._1
+ level.foldLeft((graph, 0.0)) {
+ case ((g, x), v) =>
+ val info = g.get_node(v)
+ val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
+ val x1 = x + info.width + metrics.gap
+ (g1, x1)
+ }._1
val y2 = y1 + metrics.level_height2(num_lines, num_edges)
(graph1, y2)
- })._1
+ }._1
/* pendulum/rubberband layout */
@@ -188,37 +190,41 @@
options: Options, graph: Graph, levels: List[Level]): List[Level] =
{
def resort(parent: Level, child: Level, top_down: Boolean): Level =
- child.map(v => {
- val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
- val weight =
- (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
- (v, weight)
+ child.map(v =>
+ {
+ val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
+ val weight =
+ ps.foldLeft(0.0) { case (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
+ (v, weight)
}).sortBy(_._2).map(_._1)
- ((levels, count_crossings(graph, levels)) /:
- (1 to (2 * options.int("graphview_iterations_minimize_crossings")))) {
- case ((old_levels, old_crossings), iteration) =>
- val top_down = (iteration % 2 == 1)
- val new_levels =
- if (top_down)
- (List(old_levels.head) /: old_levels.tail)((tops, bot) =>
- resort(tops.head, bot, top_down) :: tops).reverse
- else {
- val rev_old_levels = old_levels.reverse
- (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) =>
- resort(bots.head, top, top_down) :: bots)
- }
- val new_crossings = count_crossings(graph, new_levels)
- if (new_crossings < old_crossings)
- (new_levels, new_crossings)
- else
- (old_levels, old_crossings)
- }._1
+ (1 to (2 * options.int("graphview_iterations_minimize_crossings"))).
+ foldLeft((levels, count_crossings(graph, levels))) {
+ case ((old_levels, old_crossings), iteration) =>
+ val top_down = (iteration % 2 == 1)
+ val new_levels =
+ if (top_down) {
+ old_levels.tail.foldLeft(List(old_levels.head)) {
+ case (tops, bot) => resort(tops.head, bot, top_down) :: tops
+ }.reverse
+ }
+ else {
+ val rev_old_levels = old_levels.reverse
+ rev_old_levels.tail.foldLeft(List(rev_old_levels.head)) {
+ case (bots, top) => resort(bots.head, top, top_down) :: bots
+ }
+ }
+ val new_crossings = count_crossings(graph, new_levels)
+ if (new_crossings < old_crossings)
+ (new_levels, new_crossings)
+ else
+ (old_levels, old_crossings)
+ }._1
}
private def level_list(levels: Levels): List[Level] =
{
- val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
+ val max_lev = levels.foldLeft(-1) { case (m, (_, l)) => m max l }
val buckets = new Array[Level](max_lev + 1)
for (l <- 0 to max_lev) { buckets(l) = Nil }
for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
@@ -260,7 +266,7 @@
}).sum / content.length).round.toDouble
def move(graph: Graph, dx: Double): Graph =
- if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx))
+ if (dx == 0.0) graph else content.foldLeft(graph)(move_vertex(_, _, dx))
def combine(that: Region): Region = new Region(content ::: that.content)
}
@@ -289,7 +295,7 @@
def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) =
{
- ((graph, false) /: level.indices) {
+ level.indices.foldLeft((graph, false)) {
case ((graph, moved), i) =>
val r = level(i)
val d = r.deflection(graph, top_down)
@@ -307,22 +313,23 @@
val initial_regions = levels.map(level => level.map(l => new Region(List(l))))
- ((levels_graph, initial_regions, true) /:
- (1 to (2 * options.int("graphview_iterations_pendulum")))) {
- case ((graph, regions, moved), iteration) =>
- val top_down = (iteration % 2 == 1)
- if (moved) {
- val (graph1, regions1, moved1) =
- ((graph, List.empty[List[Region]], false) /:
- (if (top_down) regions else regions.reverse)) { case ((graph, tops, moved), bot) =>
- val bot1 = combine_regions(graph, top_down, bot)
- val (graph1, moved1) = deflect(bot1, top_down, graph)
- (graph1, bot1 :: tops, moved || moved1)
- }
- (graph1, regions1.reverse, moved1)
- }
- else (graph, regions, moved)
- }._1
+ (1 to (2 * options.int("graphview_iterations_pendulum"))).
+ foldLeft((levels_graph, initial_regions, true)) {
+ case ((graph, regions, moved), iteration) =>
+ val top_down = (iteration % 2 == 1)
+ if (moved) {
+ val (graph1, regions1, moved1) =
+ (if (top_down) regions else regions.reverse).
+ foldLeft((graph, List.empty[List[Region]], false)) {
+ case ((graph, tops, moved), bot) =>
+ val bot1 = combine_regions(graph, top_down, bot)
+ val (graph1, moved1) = deflect(bot1, top_down, graph)
+ (graph1, bot1 :: tops, moved || moved1)
+ }
+ (graph1, regions1.reverse, moved1)
+ }
+ else (graph, regions, moved)
+ }._1
}
@@ -346,18 +353,19 @@
{
val gap = metrics.gap
- (graph /: (1 to (2 * options.int("graphview_iterations_rubberband")))) { case (graph, _) =>
- (graph /: levels) { case (graph, level) =>
- val m = level.length - 1
- (graph /: level.iterator.zipWithIndex) {
- case (g, (v, i)) =>
- val d = force_weight(g, v)
- if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
- d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
- move_vertex(g, v, d.round.toDouble)
- else g
+ (1 to (2 * options.int("graphview_iterations_rubberband"))).foldLeft(graph) {
+ case (graph, _) =>
+ levels.foldLeft(graph) { case (graph, level) =>
+ val m = level.length - 1
+ level.iterator.zipWithIndex.foldLeft(graph) {
+ case (g, (v, i)) =>
+ val d = force_weight(g, v)
+ if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
+ d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
+ move_vertex(g, v, d.round.toDouble)
+ else g
+ }
}
- }
}
}
}
--- a/src/Tools/Graphview/metrics.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/metrics.scala Fri Mar 05 08:22:34 2021 +0100
@@ -46,7 +46,8 @@
def dummy_size2: Double = (char_width / 2).ceil
def node_width2(lines: List[String]): Double =
- (((0.0 /: lines)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2).ceil
+ ((lines.foldLeft(0.0)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2)
+ .ceil
def node_height2(num_lines: Int): Double =
((height.ceil * (num_lines max 1) + char_width) / 2).ceil
--- a/src/Tools/Graphview/model.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/model.scala Fri Mar 05 08:22:34 2021 +0100
@@ -54,7 +54,7 @@
full_graph.keys_iterator.find(node => node.ident == ident)
def make_visible_graph(): Graph_Display.Graph =
- (full_graph /: Mutators()) {
+ Mutators().foldLeft(full_graph) {
case (g, m) => if (!m.enabled) g else m.mutator.mutate(full_graph, g)
}
@@ -64,9 +64,9 @@
private def build_colors(): Unit =
{
_colors =
- (Map.empty[Graph_Display.Node, Color] /: Colors()) {
+ Colors().foldLeft(Map.empty[Graph_Display.Node, Color]) {
case (colors, m) =>
- (colors /: m.mutator.mutate(full_graph, full_graph).keys_iterator) {
+ m.mutator.mutate(full_graph, full_graph).keys_iterator.foldLeft(colors) {
case (colors, node) => colors + (node -> m.color)
}
}
--- a/src/Tools/Graphview/mutator.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/mutator.scala Fri Mar 05 08:22:34 2021 +0100
@@ -51,10 +51,11 @@
extends Graph_Filter(
name,
description,
- g => (g /: g.dest) {
+ g => g.dest.foldLeft(g) {
case (graph, ((from, _), tos)) =>
- (graph /: tos)((gr, to) =>
- if (pred(gr, (from, to))) gr else gr.del_edge(from, to))
+ tos.foldLeft(graph) {
+ case (gr, to) => if (pred(gr, (from, to))) gr else gr.del_edge(from, to)
+ }
})
class Node_Family_Filter(
@@ -116,26 +117,24 @@
{
// Add Nodes
val with_nodes =
- (to /: keys)((graph, key) => graph.default_node(key, from.get_node(key)))
+ keys.foldLeft(to) { case (graph, key) => graph.default_node(key, from.get_node(key)) }
// Add Edges
- (with_nodes /: keys) {
- (gv, key) => {
+ keys.foldLeft(with_nodes) {
+ case (gv, key) =>
def add_edges(g: Graph_Display.Graph, keys: from.Keys, succs: Boolean) =
- (g /: keys) {
- (graph, end) => {
+ keys.foldLeft(g) {
+ case (graph, end) =>
if (!graph.keys_iterator.contains(end)) graph
else {
if (succs) graph.add_edge(key, end)
else graph.add_edge(end, key)
}
- }
}
add_edges(
add_edges(gv, from.imm_preds(key), false),
from.imm_succs(key), true)
- }
}
}
--- a/src/Tools/Graphview/mutator_dialog.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala Fri Mar 05 08:22:34 2021 +0100
@@ -46,7 +46,7 @@
override def open(): Unit =
{
if (!visible) panels = get_panels(container())
- super.open
+ super.open()
}
minimumSize = new Dimension(700, 200)
@@ -94,8 +94,8 @@
def paint_panels(): Unit =
{
- Focus_Traveral_Policy.clear
- filter_panel.contents.clear
+ Focus_Traveral_Policy.clear()
+ filter_panel.contents.clear()
panels.map(x => {
filter_panel.contents += x
Focus_Traveral_Policy.addAll(x.focusList)
@@ -106,8 +106,8 @@
Focus_Traveral_Policy.add(add_button.peer)
Focus_Traveral_Policy.add(apply_button.peer)
Focus_Traveral_Policy.add(cancel_button.peer)
- filter_panel.revalidate
- filter_panel.repaint
+ filter_panel.revalidate()
+ filter_panel.repaint()
}
val filter_panel: BoxPanel = new BoxPanel(Orientation.Vertical) {}
@@ -130,7 +130,7 @@
}
private val cancel_button = new Button {
- action = Action("Close") { close }
+ action = Action("Close") { close() }
}
defaultButton = cancel_button
--- a/src/Tools/Graphview/shapes.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/Graphview/shapes.scala Fri Mar 05 08:22:34 2021 +0100
@@ -55,7 +55,7 @@
gfx.setFont(metrics.font)
val text_width =
- (0.0 /: info.lines) { case (w, line) => w max metrics.string_bounds(line).getWidth }
+ info.lines.foldLeft(0.0) { case (w, line) => w max metrics.string_bounds(line).getWidth }
val text_height =
(info.lines.length max 1) * metrics.height.ceil
val x = (s.getCenterX - text_width / 2).round.toInt
@@ -126,7 +126,7 @@
val dy = coords(2).y - coords(0).y
val (dx2, dy2) =
- ((dx, dy) /: coords.sliding(3)) {
+ coords.sliding(3).foldLeft((dx, dy)) {
case ((dx, dy), List(l, m, r)) =>
val dx2 = r.x - l.x
val dy2 = r.y - l.y
--- a/src/Tools/VSCode/src/language_server.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Fri Mar 05 08:22:34 2021 +0100
@@ -136,7 +136,7 @@
val (invoke_input, invoke_load) =
resources.resolve_dependencies(session, editor, file_watcher)
if (invoke_input) delay_input.invoke()
- if (invoke_load) delay_load.invoke
+ if (invoke_load) delay_load.invoke()
}
private val file_watcher =
@@ -307,7 +307,7 @@
try {
Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options),
- modes = modes, logic = base_info.session).await_startup
+ modes = modes, logic = base_info.session).await_startup()
reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")")
}
catch { case ERROR(msg) => reply_error(msg) }
--- a/src/Tools/VSCode/src/preview_panel.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala Fri Mar 05 08:22:34 2021 +0100
@@ -24,22 +24,23 @@
pending.change_result(map =>
{
val map1 =
- (map /: map.iterator)({ case (m, (file, column)) =>
- resources.get_model(file) match {
- case Some(model) =>
- val snapshot = model.snapshot()
- if (snapshot.is_outdated) m
- else {
- val html_context = Presentation.html_context()
- val document =
- Presentation.html_document(
- resources, snapshot, html_context, Presentation.elements2)
- channel.write(LSP.Preview_Response(file, column, document.title, document.content))
- m - file
- }
- case None => m - file
- }
- })
+ map.iterator.foldLeft(map) {
+ case (m, (file, column)) =>
+ resources.get_model(file) match {
+ case Some(model) =>
+ val snapshot = model.snapshot()
+ if (snapshot.is_outdated) m
+ else {
+ val html_context = Presentation.html_context()
+ val document =
+ Presentation.html_document(
+ resources, snapshot, html_context, Presentation.elements2)
+ channel.write(LSP.Preview_Response(file, column, document.title, document.content))
+ m - file
+ }
+ case None => m - file
+ }
+ }
(map1.nonEmpty, map1)
})
}
--- a/src/Tools/VSCode/src/vscode_rendering.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Fri Mar 05 08:22:34 2021 +0100
@@ -23,7 +23,7 @@
colors: List[Text.Info[Rendering.Color.Value]]): List[VSCode_Model.Decoration] =
{
val color_ranges =
- (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) {
+ colors.foldLeft(Map.empty[Rendering.Color.Value, List[Text.Range]]) {
case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil)))
}
types.toList.map(c =>
@@ -324,7 +324,7 @@
Text.Info(entry_range, (entry, model)) <- bibtex_entries_iterator()
if entry == name
} yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
- if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
+ if (iterator.isEmpty) None else Some(iterator.foldLeft(links)(_ :+ _))
case _ => None
}) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
--- a/src/Tools/VSCode/src/vscode_resources.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Mar 05 08:22:34 2021 +0100
@@ -28,8 +28,8 @@
def update_models(changed: Iterable[(JFile, VSCode_Model)]): State =
copy(
models = models ++ changed,
- pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file },
- pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file })
+ pending_input = changed.foldLeft(pending_input) { case (set, (file, _)) => set + file },
+ pending_output = changed.foldLeft(pending_output) { case (set, (file, _)) => set + file })
def update_caret(new_caret: Option[(JFile, Line.Position)]): State =
if (caret == new_caret) this
--- a/src/Tools/jEdit/src-base/jedit_lib.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src-base/jedit_lib.scala Fri Mar 05 08:22:34 2021 +0100
@@ -19,7 +19,7 @@
val view = if (alt_view != null) alt_view else jEdit.getActiveView()
if (view != null) {
val text_area = view.getTextArea
- if (text_area != null) text_area.requestFocus
+ if (text_area != null) text_area.requestFocus()
}
}
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/active.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/active.scala Fri Mar 05 08:22:34 2021 +0100
@@ -95,7 +95,7 @@
Isabelle.insert_line_padding(text_area, text)
else text_area.setSelectedText(text)
}
- text_area.requestFocus
+ text_area.requestFocus()
}
true
--- a/src/Tools/jEdit/src/completion_popup.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Mar 05 08:22:34 2021 +0100
@@ -281,7 +281,7 @@
{
if (view.getKeyEventInterceptor == inner_key_listener)
view.setKeyEventInterceptor(null)
- if (focus) text_area.requestFocus
+ if (focus) text_area.requestFocus()
JEdit_Lib.invalidate_range(text_area, range)
}
}
@@ -501,7 +501,7 @@
override def propagate(evt: KeyEvent): Unit =
if (!evt.isConsumed) text_field.processKeyEvent(evt)
override def shutdown(focus: Boolean): Unit =
- if (focus) text_field.requestFocus
+ if (focus) text_field.requestFocus()
}
dismissed()
completion_popup = Some(completion)
@@ -703,7 +703,7 @@
private def show_popup(focus: Boolean): Unit =
{
popup.show
- if (focus) list_view.requestFocus
+ if (focus) list_view.requestFocus()
}
private def hide_popup(): Unit =
--- a/src/Tools/jEdit/src/debugger_dockable.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Fri Mar 05 08:22:34 2021 +0100
@@ -298,7 +298,7 @@
/* focus */
- override def focusOnDefaultComponent(): Unit = eval_button.requestFocus
+ override def focusOnDefaultComponent(): Unit = eval_button.requestFocus()
addFocusListener(new FocusAdapter {
override def focusGained(e: FocusEvent): Unit = update_focus()
--- a/src/Tools/jEdit/src/document_model.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Mar 05 08:22:34 2021 +0100
@@ -592,7 +592,7 @@
val edits = get_edits
val (reparse, perspective) = node_perspective(doc_blobs, hidden)
if (reparse || edits.nonEmpty || last_perspective != perspective) {
- pending.clear
+ pending.clear()
last_perspective = perspective
node_edits(node_header(), edits, perspective)
}
--- a/src/Tools/jEdit/src/isabelle.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Mar 05 08:22:34 2021 +0100
@@ -616,5 +616,5 @@
/* java monitor */
def java_monitor(view: View): Unit =
- Java_Monitor.java_monitor_external(view, look_and_feel = GUI.current_laf())
+ Java_Monitor.java_monitor_external(view, look_and_feel = GUI.current_laf)
}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Mar 05 08:22:34 2021 +0100
@@ -121,18 +121,19 @@
offset: Text.Offset,
documents: List[Document_Structure.Document]): Unit =
{
- documents.foldLeft(offset) { case (i, document) =>
- document match {
- case Document_Structure.Block(name, text, body) =>
- val range = Text.Range(i, i + document.length)
- val node =
- new DefaultMutableTreeNode(
- new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
- parent.add(node)
- make_tree(node, i, body)
- case _ =>
- }
- i + document.length
+ documents.foldLeft(offset) {
+ case (i, document) =>
+ document match {
+ case Document_Structure.Block(name, text, body) =>
+ val range = Text.Range(i, i + document.length)
+ val node =
+ new DefaultMutableTreeNode(
+ new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
+ parent.add(node)
+ make_tree(node, i, body)
+ case _ =>
+ }
+ i + document.length
}
}
@@ -179,7 +180,7 @@
{
val opt_snapshot =
Document_Model.get(buffer) match {
- case Some(model) if model.is_theory => Some(model.snapshot)
+ case Some(model) if model.is_theory => Some(model.snapshot())
case _ => None
}
opt_snapshot match {
--- a/src/Tools/jEdit/src/jedit_editor.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Mar 05 08:22:34 2021 +0100
@@ -66,7 +66,7 @@
{
GUI_Thread.require {}
Document_Model.get(name) match {
- case Some(model) => model.snapshot
+ case Some(model) => model.snapshot()
case None => session.snapshot(name)
}
}
--- a/src/Tools/jEdit/src/jedit_lib.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Mar 05 08:22:34 2021 +0100
@@ -50,7 +50,7 @@
dummy_window.setContentPane(outer)
dummy_window.pack
- dummy_window.revalidate
+ dummy_window.revalidate()
val geometry =
Window_Geometry(
--- a/src/Tools/jEdit/src/jedit_sessions.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Mar 05 08:22:34 2021 +0100
@@ -18,10 +18,10 @@
{
/* session options */
- def session_dirs(): List[Path] =
+ def session_dirs: List[Path] =
Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-")
- def session_no_build(): Boolean =
+ def session_no_build: Boolean =
Isabelle_System.getenv("JEDIT_NO_BUILD") == "true"
def session_options(options: Options): Options =
@@ -41,7 +41,7 @@
options2
}
- def sessions_structure(options: Options, dirs: List[Path] = session_dirs()): Sessions.Structure =
+ def sessions_structure(options: Options, dirs: List[Path] = session_dirs): Sessions.Structure =
Sessions.load_structure(session_options(options), dirs = dirs)
@@ -119,7 +119,7 @@
def session_base_info(options: Options): Sessions.Base_Info =
Sessions.base_info(options,
- dirs = JEdit_Sessions.session_dirs(),
+ dirs = JEdit_Sessions.session_dirs,
include_sessions = logic_include_sessions,
session = logic_name(options),
session_ancestor = logic_ancestor,
@@ -130,7 +130,7 @@
{
Build.build(session_options(options),
selection = Sessions.Selection.session(PIDE.resources.session_name),
- progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs(),
+ progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs,
infos = PIDE.resources.session_base_info.infos).rc
}
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Fri Mar 05 08:22:34 2021 +0100
@@ -87,7 +87,7 @@
val option_name = "spell_checker_dictionary"
val opt = PIDE.options.value.check_name(option_name)
- val entries = Spell_Checker.dictionaries()
+ val entries = Spell_Checker.dictionaries
val component = new ComboBox(entries) with Option_Component {
name = option_name
val title = opt.title()
--- a/src/Tools/jEdit/src/plugin.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Mar 05 08:22:34 2021 +0100
@@ -29,7 +29,7 @@
def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now
{
val buffer = JEdit_Lib.jedit_view(view).getBuffer
- Document_Model.get(buffer).map(_.snapshot)
+ Document_Model.get(buffer).map(_.snapshot())
}
def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now
@@ -393,7 +393,7 @@
case msg: PropertiesChanged =>
for {
- view <- JEdit_Lib.jedit_views
+ view <- JEdit_Lib.jedit_views()
edit_pane <- JEdit_Lib.jedit_edit_panes(view)
} {
val buffer = edit_pane.getBuffer
@@ -458,13 +458,13 @@
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
+ http_server.start()
startup_failure = None
}
@@ -483,11 +483,11 @@
override def stop(): Unit =
{
- http_server.stop
+ http_server.stop()
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_text_area.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Mar 05 08:22:34 2021 +0100
@@ -95,7 +95,7 @@
val results = current_base_results
val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric)
- future_refresh.foreach(_.cancel)
+ future_refresh.foreach(_.cancel())
future_refresh =
Some(Future.fork {
val (text, rendering) =
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Mar 05 08:22:34 2021 +0100
@@ -267,7 +267,7 @@
val h = painter.getLineHeight * lines + geometry.deco_height
val margin1 =
if (h <= h_max) {
- split_lines(XML.content(formatted)).foldLeft(0.0)({ case (m, line) => m max metric(line) })
+ split_lines(XML.content(formatted)).foldLeft(0.0) { case (m, line) => m max metric(line) }
}
else margin
val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
@@ -280,12 +280,12 @@
private def show_popup: Unit =
{
popup.show
- pretty_text_area.requestFocus
+ pretty_text_area.requestFocus()
pretty_text_area.update(rendering.snapshot, results, info.info)
}
private def hide_popup: Unit = popup.hide
- private def request_focus: Unit = pretty_text_area.requestFocus
+ private def request_focus: Unit = pretty_text_area.requestFocus()
}
--- a/src/Tools/jEdit/src/process_indicator.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/process_indicator.scala Fri Mar 05 08:22:34 2021 +0100
@@ -34,7 +34,7 @@
{
current_frame = (current_frame + 1) % active_icons.length
setImage(active_icons(current_frame))
- label.repaint
+ label.repaint()
}
})
timer.setRepeats(true)
@@ -44,7 +44,7 @@
if (rate == 0) {
setImage(passive_icon)
timer.stop
- label.repaint
+ label.repaint()
}
else {
val delay = 1000 / rate
--- a/src/Tools/jEdit/src/query_dockable.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Fri Mar 05 08:22:34 2021 +0100
@@ -258,7 +258,7 @@
def select: Unit =
{
- control_panel.contents.clear
+ control_panel.contents.clear()
control_panel.contents += query_label
update_items().foreach(item => control_panel.contents += item.checkbox)
control_panel.contents ++=
@@ -291,13 +291,13 @@
private def select_operation(): Unit =
{
- for (op <- get_operation()) { op.select; op.query.requestFocus }
- operations_pane.revalidate
+ for (op <- get_operation()) { op.select; op.query.requestFocus() }
+ operations_pane.revalidate()
}
override def focusOnDefaultComponent(): Unit =
{
- for (op <- get_operation()) op.query.requestFocus
+ for (op <- get_operation()) op.query.requestFocus()
}
select_operation()
--- a/src/Tools/jEdit/src/rich_text_area.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Mar 05 08:22:34 2021 +0100
@@ -221,7 +221,7 @@
case _: ArrayIndexOutOfBoundsException =>
case _: IllegalArgumentException =>
}
- text_area.requestFocus
+ text_area.requestFocus()
}
link.follow(view)
case None =>
--- a/src/Tools/jEdit/src/scala_console.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Fri Mar 05 08:22:34 2021 +0100
@@ -30,7 +30,7 @@
override def flush(): Unit =
{
- val s = buf.synchronized { val s = buf.toString; buf.clear; s }
+ val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
val str = UTF8.decode_permissive(s)
GUI_Thread.later {
if (global_out == null) System.out.print(str)
@@ -97,7 +97,7 @@
private class Interpreter
{
private val running = Synchronized[Option[Thread]](None)
- def interrupt: Unit = running.change(opt => { opt.foreach(_.interrupt); opt })
+ def interrupt(): Unit = running.change(opt => { opt.foreach(_.interrupt()); opt })
private val interp =
Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
@@ -146,8 +146,8 @@
{
interpreters.get(console) match {
case Some(interp) =>
- interp.interrupt
- interp.thread.shutdown
+ interp.interrupt()
+ interp.thread.shutdown()
interpreters -= console
case None =>
}
@@ -177,5 +177,5 @@
}
override def stop(console: Console): Unit =
- interpreters.get(console).foreach(_.interrupt)
+ interpreters.get(console).foreach(_.interrupt())
}
--- a/src/Tools/jEdit/src/session_build.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Fri Mar 05 08:22:34 2021 +0100
@@ -80,10 +80,10 @@
private def set_actions(cs: Component*): Unit =
{
- action_panel.contents.clear
+ action_panel.contents.clear()
action_panel.contents ++= cs
- layout_panel.revalidate
- layout_panel.repaint
+ layout_panel.revalidate()
+ layout_panel.repaint()
}
@@ -94,7 +94,7 @@
private def return_code(rc: Int): Unit =
GUI_Thread.later {
_return_code = Some(rc)
- delay_exit.invoke
+ delay_exit.invoke()
}
private val delay_exit =
@@ -129,7 +129,7 @@
private def stopping(): Unit =
{
- progress.stop
+ progress.stop()
set_actions(new Label("Stopping ..."))
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Mar 05 08:22:34 2021 +0100
@@ -145,7 +145,7 @@
add(controls.peer, BorderLayout.NORTH)
- override def focusOnDefaultComponent(): Unit = provers.requestFocus
+ override def focusOnDefaultComponent(): Unit = provers.requestFocus()
/* main */
--- a/src/Tools/jEdit/src/symbols_dockable.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Fri Mar 05 08:22:34 2021 +0100
@@ -43,7 +43,7 @@
Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt))
text_area.setSelectedText(s1 + s2)
text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
- text_area.requestFocus
+ text_area.requestFocus()
}
tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
}
@@ -67,12 +67,12 @@
forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
} yield (txt, abbr)): _*).iterator_list.toList
- contents.clear
+ contents.clear()
for ((txt, abbrs) <- entries.sortBy(_._1))
contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
- revalidate
- repaint
+ revalidate()
+ repaint()
}
}
@@ -101,7 +101,7 @@
Syntax_Style.edit_control_style(text_area, symbol)
else
text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol))
- text_area.requestFocus
+ text_area.requestFocus()
}
tooltip =
GUI.tooltip_lines(
@@ -113,7 +113,7 @@
action = Action("Reset") {
val text_area = view.getTextArea
Syntax_Style.edit_control_style(text_area, "")
- text_area.requestFocus
+ text_area.requestFocus()
}
tooltip = "Reset control symbols within text"
}
@@ -135,14 +135,14 @@
val results =
for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
- results_panel.contents.clear
+ results_panel.contents.clear()
for (sym <- results.take(search_limit))
results_panel.contents += new Symbol_Component(sym, false)
if (results.length > search_limit)
results_panel.contents +=
new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
- revalidate
- repaint
+ revalidate()
+ repaint()
}
search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
}
@@ -170,7 +170,7 @@
listenTo(selection)
reactions += {
case SelectionChanged(_) if selection.page == search_page =>
- search_panel.search_field.requestFocus
+ search_panel.search_field.requestFocus()
}
for (page <- pages)
--- a/src/Tools/jEdit/src/text_overview.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Fri Mar 05 08:22:34 2021 +0100
@@ -116,7 +116,7 @@
private def is_running(): Boolean = !future_refresh.value.is_finished
def invoke(): Unit = delay_refresh.invoke()
- def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) }
+ def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel(); x }) }
private val delay_refresh =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {
--- a/src/Tools/jEdit/src/text_structure.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala Fri Mar 05 08:22:34 2021 +0100
@@ -93,7 +93,7 @@
(for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
doc_view <- Document_View.get(text_area)
- } yield doc_view.get_rendering).nextOption()
+ } yield doc_view.get_rendering()).nextOption()
}
else None
val limit = PIDE.options.value.int("jedit_indent_script_limit")
@@ -130,11 +130,12 @@
}).collectFirst({ case (i, true) => i }).getOrElse(0)
def indent_brackets: Int =
- prev_line_span.foldLeft(0)(
- { case (i, tok) =>
- if (tok.is_open_bracket) i + indent_size
- else if (tok.is_close_bracket) i - indent_size
- else i })
+ prev_line_span.foldLeft(0) {
+ case (i, tok) =>
+ if (tok.is_open_bracket) i + indent_size
+ else if (tok.is_close_bracket) i - indent_size
+ else i
+ }
def indent_extra: Int =
if (prev_span.exists(keywords.is_quasi_command)) indent_size
--- a/src/Tools/jEdit/src/theories_dockable.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Fri Mar 05 08:22:34 2021 +0100
@@ -25,7 +25,7 @@
{
/* status */
- private val status = new ListView(Nil: List[Document.Node.Name]) {
+ private val status = new ListView(List.empty[Document.Node.Name]) {
background =
{
// enforce default value
@@ -159,11 +159,12 @@
(node_status.failed, PIDE.options.color_value("error_color"))
).filter(_._1 > 0)
- segments.foldLeft(size.width - 2)({ case (last, (n, color)) =>
- val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
- paint_segment(last - w, w, color)
- last - w - 1
- })
+ segments.foldLeft(size.width - 2) {
+ case (last, (n, color)) =>
+ val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
+ paint_segment(last - w, w, color)
+ last - w - 1
+ }
case None =>
paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
--- a/src/Tools/jEdit/src/timing_dockable.scala Thu Mar 04 18:38:56 2021 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Fri Mar 05 08:22:34 2021 +0100
@@ -104,7 +104,7 @@
/* timing view */
- private val timing_view = new ListView(Nil: List[Entry]) {
+ private val timing_view = new ListView(List.empty[Entry]) {
listenTo(mouse.clicks)
reactions += {
case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
@@ -186,9 +186,8 @@
(restriction match {
case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name)))
case None => snapshot.version.nodes.iterator
- })
- .foldLeft(nodes_timing)(
- { case (timing1, (name, node)) =>
+ }).foldLeft(nodes_timing) {
+ case (timing1, (name, node)) =>
if (PIDE.resources.session_base.loaded_theory(name)) timing1
else {
val node_timing =
@@ -196,7 +195,7 @@
snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
timing1 + (name -> node_timing)
}
- })
+ }
nodes_timing = nodes_timing1
val entries = make_entries()