diff --git a/src/Pure/Admin/build_cygwin.scala b/src/Pure/Admin/build_cygwin.scala --- a/src/Pure/Admin/build_cygwin.scala +++ b/src/Pure/Admin/build_cygwin.scala @@ -1,89 +1,89 @@ /* Title: Pure/Admin/build_cygwin.scala Author: Makarius Produce pre-canned Cygwin distribution for Isabelle. */ package isabelle object Build_Cygwin { val default_mirror: String = "https://isabelle.sketis.net/cygwin_2021" val packages: List[String] = List("curl", "libgmp-devel", "nano", "perl", "perl-libwww-perl", "rlwrap", "unzip") def build_cygwin(progress: Progress, mirror: String = default_mirror, more_packages: List[String] = Nil) { - require(Platform.is_windows) + require(Platform.is_windows, "Windows platform expected") Isabelle_System.with_tmp_dir("cygwin")(tmp_dir => { val cygwin = tmp_dir + Path.explode("cygwin") val cygwin_etc = cygwin + Path.explode("etc") val cygwin_isabelle = Isabelle_System.make_directory(cygwin + Path.explode("isabelle")) val cygwin_exe_name = mirror + "/setup-x86_64.exe" val cygwin_exe = cygwin_isabelle + Path.explode("cygwin.exe") Bytes.write(cygwin_exe, try { Bytes.read(Url(cygwin_exe_name)) } catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) }) File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror) File.set_executable(cygwin_exe, true) Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h /dev/null").check val res = progress.bash( File.bash_path(cygwin_exe) + " --site " + Bash.string(mirror) + " --no-verify" + " --local-package-dir 'C:\\temp'" + " --root " + File.bash_platform_path(cygwin) + " --packages " + quote((packages ::: more_packages).mkString(",")) + " --no-shortcuts --no-startmenu --no-desktop --quiet-mode", echo = true) if (!res.ok || !cygwin_etc.is_dir) error("Failed") for (name <- List("hosts", "protocols", "services", "networks", "passwd", "group")) (cygwin_etc + Path.explode(name)).file.delete (cygwin + Path.explode("Cygwin.bat")).file.delete val archive = "cygwin-" + Date.Format("uuuuMMdd")(Date.now()) + ".tar.gz" Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_cygwin", "produce pre-canned Cygwin distribution for Isabelle", Scala_Project.here, args => { var mirror = default_mirror var more_packages: List[String] = Nil val getopts = Getopts(""" Usage: isabelle build_cygwin [OPTIONS] Options are: -R MIRROR Cygwin mirror site (default """ + quote(default_mirror) + """) -p NAME additional Cygwin package Produce pre-canned Cygwin distribution for Isabelle: this requires Windows administrator mode. """, "R:" -> (arg => mirror = arg), "p:" -> (arg => more_packages ::= arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() build_cygwin(new Console_Progress(), mirror = mirror, more_packages = more_packages) }) } diff --git a/src/Pure/Admin/build_status.scala b/src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala +++ b/src/Pure/Admin/build_status.scala @@ -1,621 +1,621 @@ /* Title: Pure/Admin/build_status.scala Author: Makarius Present recent build status information from database. */ package isabelle object Build_Status { /* defaults */ val default_target_dir = Path.explode("build_status") val default_image_size = (800, 600) val default_history = 30 def default_profiles: List[Profile] = Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles /* data profiles */ sealed case class Profile( description: String, history: Int = 0, afp: Boolean = false, bulky: Boolean = false, sql: String) { def days(options: Options): Int = options.int("build_log_history") max history def stretch(options: Options): Double = (days(options) max default_history min (default_history * 5)).toDouble / default_history def select(options: Options, columns: List[SQL.Column], only_sessions: Set[String]): SQL.Source = { Build_Log.Data.universal_table.select(columns, distinct = true, sql = "WHERE " + Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) + " AND " + SQL.member(Build_Log.Data.status.ident, List( Build_Log.Session_Status.finished.toString, Build_Log.Session_Status.failed.toString)) + (if (only_sessions.isEmpty) "" else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) + " AND " + SQL.enclose(sql)) } } /* build status */ def build_status(options: Options, progress: Progress = new Progress, profiles: List[Profile] = default_profiles, only_sessions: Set[String] = Set.empty, verbose: Boolean = false, target_dir: Path = default_target_dir, ml_statistics: Boolean = false, image_size: (Int, Int) = default_image_size) { val ml_statistics_domain = Iterator(ML_Statistics.heap_fields, ML_Statistics.program_fields, ML_Statistics.tasks_fields, ML_Statistics.workers_fields).flatMap(_._2).toSet val data = read_data(options, progress = progress, profiles = profiles, only_sessions = only_sessions, verbose = verbose, ml_statistics = ml_statistics, ml_statistics_domain = ml_statistics_domain) present_data(data, progress = progress, target_dir = target_dir, image_size = image_size) } /* read data */ sealed case class Data(date: Date, entries: List[Data_Entry]) sealed case class Data_Entry( name: String, hosts: List[String], stretch: Double, sessions: List[Session]) { def failed_sessions: List[Session] = sessions.filter(_.head.failed).sortBy(_.name) } sealed case class Session( name: String, threads: Int, entries: List[Entry], ml_statistics: ML_Statistics, ml_statistics_date: Long) { - require(entries.nonEmpty) + require(entries.nonEmpty, "no entries") lazy val sorted_entries: List[Entry] = entries.sortBy(entry => - entry.date) def head: Entry = sorted_entries.head def order: Long = - head.timing.elapsed.ms def finished_entries: List[Entry] = sorted_entries.filter(_.finished) def finished_entries_size: Int = finished_entries.map(_.date).toSet.size def check_timing: Boolean = finished_entries_size >= 3 def check_heap: Boolean = finished_entries_size >= 3 && finished_entries.forall(entry => entry.maximum_heap > 0 || entry.average_heap > 0 || entry.stored_heap > 0) def make_csv: CSV.File = { val header = List("session_name", "chapter", "pull_date", "afp_pull_date", "isabelle_version", "afp_version", "timing_elapsed", "timing_cpu", "timing_gc", "ml_timing_elapsed", "ml_timing_cpu", "ml_timing_gc", "maximum_code", "average_code", "maximum_stack", "average_stack", "maximum_heap", "average_heap", "stored_heap", "status") val date_format = Date.Format("uuuu-MM-dd HH:mm:ss") val records = for (entry <- sorted_entries) yield { CSV.Record(name, entry.chapter, date_format(entry.pull_date), entry.afp_pull_date match { case Some(date) => date_format(date) case None => "" }, entry.isabelle_version, entry.afp_version, entry.timing.elapsed.ms, entry.timing.cpu.ms, entry.timing.gc.ms, entry.ml_timing.elapsed.ms, entry.ml_timing.cpu.ms, entry.ml_timing.gc.ms, entry.maximum_code, entry.average_code, entry.maximum_stack, entry.average_stack, entry.maximum_heap, entry.average_heap, entry.stored_heap, entry.status) } CSV.File(name, header, records) } } sealed case class Entry( chapter: String, pull_date: Date, afp_pull_date: Option[Date], isabelle_version: String, afp_version: String, timing: Timing, ml_timing: Timing, maximum_code: Long, average_code: Long, maximum_stack: Long, average_stack: Long, maximum_heap: Long, average_heap: Long, stored_heap: Long, status: Build_Log.Session_Status.Value, errors: List[String]) { val date: Long = (afp_pull_date getOrElse pull_date).unix_epoch def finished: Boolean = status == Build_Log.Session_Status.finished def failed: Boolean = status == Build_Log.Session_Status.failed def present_errors(name: String): XML.Body = { if (errors.isEmpty) HTML.text(name + print_version(isabelle_version, afp_version, chapter)) else { HTML.tooltip_errors(HTML.text(name), errors.map(s => HTML.text(Symbol.decode(s)))) :: HTML.text(print_version(isabelle_version, afp_version, chapter)) } } } sealed case class Image(name: String, width: Int, height: Int) { def path: Path = Path.basic(name) } def print_version( isabelle_version: String, afp_version: String = "", chapter: String = AFP.chapter): String = { val body = proper_string(isabelle_version).map("Isabelle/" + _).toList ::: (if (chapter == AFP.chapter) proper_string(afp_version).map("AFP/" + _) else None).toList if (body.isEmpty) "" else body.mkString(" (", ", ", ")") } def read_data(options: Options, progress: Progress = new Progress, profiles: List[Profile] = default_profiles, only_sessions: Set[String] = Set.empty, ml_statistics: Boolean = false, ml_statistics_domain: String => Boolean = (key: String) => true, verbose: Boolean = false): Data = { val date = Date.now() var data_hosts = Map.empty[String, Set[String]] var data_stretch = Map.empty[String, Double] var data_entries = Map.empty[String, Map[String, Session]] def get_hosts(data_name: String): Set[String] = data_hosts.getOrElse(data_name, Set.empty) val store = Build_Log.store(options) using(store.open_database())(db => { for (profile <- profiles.sortBy(_.description)) { progress.echo("input " + quote(profile.description)) val afp = profile.afp val columns = List( Build_Log.Data.pull_date(afp = false), Build_Log.Data.pull_date(afp = true), Build_Log.Prop.build_host, Build_Log.Prop.isabelle_version, Build_Log.Prop.afp_version, Build_Log.Settings.ISABELLE_BUILD_OPTIONS, Build_Log.Settings.ML_PLATFORM, Build_Log.Data.session_name, Build_Log.Data.chapter, Build_Log.Data.groups, Build_Log.Data.threads, Build_Log.Data.timing_elapsed, Build_Log.Data.timing_cpu, Build_Log.Data.timing_gc, Build_Log.Data.ml_timing_elapsed, Build_Log.Data.ml_timing_cpu, Build_Log.Data.ml_timing_gc, Build_Log.Data.heap_size, Build_Log.Data.status, Build_Log.Data.errors) ::: (if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil) val Threads_Option = """threads\s*=\s*(\d+)""".r val sql = profile.select(options, columns, only_sessions) progress.echo_if(verbose, sql) db.using_statement(sql)(stmt => { val res = stmt.execute_query() while (res.next()) { val session_name = res.string(Build_Log.Data.session_name) val chapter = res.string(Build_Log.Data.chapter) val groups = split_lines(res.string(Build_Log.Data.groups)) val threads = { val threads1 = res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match { case Threads_Option(Value.Int(i)) => i case _ => 1 } val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1) threads1 max threads2 } val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM) val data_name = profile.description + (if (ml_platform.startsWith("x86_64-")) ", 64bit" else "") + (if (threads == 1) "" else ", " + threads + " threads") res.get_string(Build_Log.Prop.build_host).foreach(host => data_hosts += (data_name -> (get_hosts(data_name) + host))) data_stretch += (data_name -> profile.stretch(options)) val isabelle_version = res.string(Build_Log.Prop.isabelle_version) val afp_version = res.string(Build_Log.Prop.afp_version) val ml_stats = ML_Statistics( if (ml_statistics) { Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics), cache = store.cache) } else Nil, domain = ml_statistics_domain, heading = session_name + print_version(isabelle_version, afp_version, chapter)) val entry = Entry( chapter = chapter, pull_date = res.date(Build_Log.Data.pull_date(afp = false)), afp_pull_date = if (afp) res.get_date(Build_Log.Data.pull_date(afp = true)) else None, isabelle_version = isabelle_version, afp_version = afp_version, timing = res.timing( Build_Log.Data.timing_elapsed, Build_Log.Data.timing_cpu, Build_Log.Data.timing_gc), ml_timing = res.timing( Build_Log.Data.ml_timing_elapsed, Build_Log.Data.ml_timing_cpu, Build_Log.Data.ml_timing_gc), maximum_code = ml_stats.maximum(ML_Statistics.CODE_SIZE).toLong, average_code = ml_stats.average(ML_Statistics.CODE_SIZE).toLong, maximum_stack = ml_stats.maximum(ML_Statistics.STACK_SIZE).toLong, average_stack = ml_stats.average(ML_Statistics.STACK_SIZE).toLong, maximum_heap = ml_stats.maximum(ML_Statistics.HEAP_SIZE).toLong, average_heap = ml_stats.average(ML_Statistics.HEAP_SIZE).toLong, stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)), status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)), errors = Build_Log.uncompress_errors( res.bytes(Build_Log.Data.errors), cache = store.cache)) val sessions = data_entries.getOrElse(data_name, Map.empty) val session = sessions.get(session_name) match { case None => Session(session_name, threads, List(entry), ml_stats, entry.date) case Some(old) => val (ml_stats1, ml_stats1_date) = if (entry.date > old.ml_statistics_date) (ml_stats, entry.date) else (old.ml_statistics, old.ml_statistics_date) Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date) } if ((!afp || chapter == AFP.chapter) && (!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) { data_entries += (data_name -> (sessions + (session_name -> session))) } } }) } }) val sorted_entries = (for { (name, sessions) <- data_entries.toList sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order)) } yield { val hosts = get_hosts(name).toList.sorted val stretch = data_stretch(name) Data_Entry(name, hosts, stretch, sorted_sessions) }).sortBy(_.name) Data(date, sorted_entries) } /* present data */ def present_data(data: Data, progress: Progress = new Progress, target_dir: Path = default_target_dir, image_size: (Int, Int) = default_image_size) { def clean_name(name: String): String = name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString) HTML.write_document(target_dir, "index.html", List(HTML.title("Isabelle build status")), List(HTML.chapter("Isabelle build status"), HTML.par( List(HTML.description( List(HTML.text("status date:") -> HTML.text(data.date.toString))))), HTML.par( List(HTML.itemize(data.entries.map({ case data_entry => List( HTML.link(clean_name(data_entry.name) + "/index.html", HTML.text(data_entry.name))) ::: (data_entry.failed_sessions match { case Nil => Nil case sessions => HTML.break ::: List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) ::: List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name)))) }) })))))) for (data_entry <- data.entries) { val data_name = data_entry.name val (image_width, image_height) = image_size val image_width_stretch = (image_width * data_entry.stretch).toInt progress.echo("output " + quote(data_name)) val dir = Isabelle_System.make_directory(target_dir + Path.basic(clean_name(data_name))) val data_files = (for (session <- data_entry.sessions) yield { val csv_file = session.make_csv csv_file.write(dir) session.name -> csv_file }).toMap val session_plots = Par_List.map((session: Session) => Isabelle_System.with_tmp_file(session.name, "data") { data_file => Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file => def plot_name(kind: String): String = session.name + "_" + kind + ".png" File.write(data_file, cat_lines( session.finished_entries.map(entry => List(entry.date, entry.timing.elapsed.minutes, entry.timing.resources.minutes, entry.ml_timing.elapsed.minutes, entry.ml_timing.resources.minutes, entry.maximum_code, entry.maximum_code, entry.average_stack, entry.maximum_stack, entry.average_heap, entry.average_heap, entry.stored_heap).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 val timing_range = "[0:" + max_time + "]" def gnuplot(plot_name: String, plots: List[String], range: String): Image = { val image = Image(plot_name, image_width_stretch, image_height) File.write(gnuplot_file, """ set terminal png size """ + image.width + "," + image.height + """ set output """ + quote(File.standard_path(dir + image.path)) + """ set xdata time set timefmt "%s" set format x "%d-%b" set xlabel """ + quote(session.name) + """ noenhanced set key left bottom plot [] """ + range + " " + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n") val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file)) if (!result.ok) result.error("Gnuplot failed for " + data_name + "/" + plot_name).check image } val timing_plots = { val plots1 = List( """ using 1:2 smooth sbezier title "elapsed time (smooth)" """, """ using 1:2 smooth csplines title "elapsed time" """) val plots2 = List( """ using 1:3 smooth sbezier title "cpu time (smooth)" """, """ using 1:3 smooth csplines title "cpu time" """) if (session.threads == 1) plots1 else plots1 ::: plots2 } val ml_timing_plots = List( """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """, """ using 1:4 smooth csplines title "ML elapsed time" """, """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """, """ using 1:5 smooth csplines title "ML cpu time" """) val heap_plots = List( """ using 1:10 smooth sbezier title "heap maximum (smooth)" """, """ using 1:10 smooth csplines title "heap maximum" """, """ using 1:11 smooth sbezier title "heap average (smooth)" """, """ using 1:11 smooth csplines title "heap average" """, """ using 1:12 smooth sbezier title "heap stored (smooth)" """, """ using 1:12 smooth csplines title "heap stored" """) def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image = { val image = Image(plot_name, image_width, image_height) val chart = session.ml_statistics.chart( fields._1 + ": " + session.ml_statistics.heading, fields._2) Graphics_File.write_chart_png( (dir + image.path).file, chart, image.width, image.height) image } val images = (if (session.check_timing) List( gnuplot(plot_name("timing"), timing_plots, timing_range), gnuplot(plot_name("ml_timing"), ml_timing_plots, timing_range)) else Nil) ::: (if (session.check_heap) List(gnuplot(plot_name("heap"), heap_plots, "[0:]")) else Nil) ::: (if (session.ml_statistics.content.nonEmpty) List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields), jfreechart(plot_name("program_chart"), ML_Statistics.program_fields)) ::: (if (session.threads > 1) List( jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields), jfreechart(plot_name("workers_chart"), ML_Statistics.workers_fields)) else Nil) else Nil) session.name -> images } }, data_entry.sessions).toMap HTML.write_document(dir, "index.html", List(HTML.title("Isabelle build status for " + data_name)), HTML.chapter("Isabelle build status for " + data_name) :: HTML.par( List(HTML.description( List( HTML.text("status date:") -> HTML.text(data.date.toString), HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) :: HTML.par( List(HTML.itemize( data_entry.sessions.map(session => HTML.link("#session_" + session.name, HTML.text(session.name)) :: HTML.text(" (" + session.head.timing.message_resources + ")"))))) :: data_entry.sessions.flatMap(session => List( HTML.section(HTML.id("session_" + session.name), session.name), HTML.par( HTML.description( List( HTML.text("data:") -> List(HTML.link(data_files(session.name).file_name, HTML.text("CSV"))), HTML.text("timing:") -> HTML.text(session.head.timing.message_resources), HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) ::: ML_Statistics.mem_print(session.head.maximum_code).map(s => HTML.text("code maximum:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.average_code).map(s => HTML.text("code average:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.maximum_stack).map(s => HTML.text("stack maximum:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.average_stack).map(s => HTML.text("stack average:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.maximum_heap).map(s => HTML.text("heap maximum:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.average_heap).map(s => HTML.text("heap average:") -> HTML.text(s)).toList ::: ML_Statistics.mem_print(session.head.stored_heap).map(s => HTML.text("heap stored:") -> HTML.text(s)).toList ::: proper_string(session.head.isabelle_version).map(s => HTML.text("Isabelle version:") -> HTML.text(s)).toList ::: proper_string(session.head.afp_version).map(s => HTML.text("AFP version:") -> HTML.text(s)).toList) :: session_plots.getOrElse(session.name, Nil).map(image => HTML.size(image.width / 2, image.height / 2)(HTML.image(image.name))))))) } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_status", "present recent build status information from database", Scala_Project.here, args => { var target_dir = default_target_dir var ml_statistics = false var only_sessions = Set.empty[String] var options = Options.init() var image_size = default_image_size var verbose = false val getopts = Getopts(""" Usage: isabelle build_status [OPTIONS] Options are: -D DIR target directory (default """ + default_target_dir + """) -M include full ML statistics -S SESSIONS only given SESSIONS (comma separated) -l DAYS length of relevant history (default """ + options.int("build_log_history") + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -s WxH size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """) -v verbose Present performance statistics from build log database, which is specified via system options build_log_database_host, build_log_database_user, build_log_history etc. """, "D:" -> (arg => target_dir = Path.explode(arg)), "M" -> (_ => ml_statistics = true), "S:" -> (arg => only_sessions = space_explode(',', arg).toSet), "l:" -> (arg => options = options + ("build_log_history=" + arg)), "o:" -> (arg => options = options + arg), "s:" -> (arg => space_explode('x', arg).map(Value.Int.parse(_)) match { case List(w, h) if w > 0 && h > 0 => image_size = (w, h) case _ => error("Error bad PNG image size: " + quote(arg)) }), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose, target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size) }) } diff --git a/src/Pure/Concurrent/counter.scala b/src/Pure/Concurrent/counter.scala --- a/src/Pure/Concurrent/counter.scala +++ b/src/Pure/Concurrent/counter.scala @@ -1,29 +1,29 @@ /* Title: Pure/Concurrent/counter.scala Author: Makarius Synchronized counter for unique identifiers < 0. NB: ML ticks forwards, JVM ticks backwards. */ package isabelle object Counter { type ID = Long def make(): Counter = new Counter } final class Counter private { private var count: Counter.ID = 0 def apply(): Counter.ID = synchronized { - require(count > java.lang.Long.MIN_VALUE) + require(count > java.lang.Long.MIN_VALUE, "counter overflow") count -= 1 count } override def toString: String = count.toString } diff --git a/src/Pure/Concurrent/future.scala b/src/Pure/Concurrent/future.scala --- a/src/Pure/Concurrent/future.scala +++ b/src/Pure/Concurrent/future.scala @@ -1,161 +1,161 @@ /* Title: Pure/Concurrent/future.scala Author: Makarius Value-oriented parallel execution via futures and promises. */ package isabelle import java.util.concurrent.Callable /* futures and promises */ object Future { def value[A](x: A): Future[A] = new Value_Future(x) def fork[A](body: => A): Future[A] = new Task_Future[A](body) def promise[A]: Promise[A] = new Promise_Future[A] def thread[A]( name: String = "", group: ThreadGroup = Isabelle_Thread.current_thread_group, pri: Int = Thread.NORM_PRIORITY, daemon: Boolean = false, inherit_locals: Boolean = false, uninterruptible: Boolean = false)(body: => A): Future[A] = { new Thread_Future[A](name, group, pri, daemon, inherit_locals, uninterruptible, body) } } trait Future[A] { def peek: Option[Exn.Result[A]] def is_finished: Boolean = peek.isDefined - def get_finished: A = { require(is_finished); Exn.release(peek.get) } + def get_finished: A = { require(is_finished, "future not finished"); Exn.release(peek.get) } 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 override def toString: String = peek match { case None => "" case Some(Exn.Exn(_)) => "" case Some(Exn.Res(x)) => x.toString } } trait Promise[A] extends Future[A] { def fulfill_result(res: Exn.Result[A]): Unit def fulfill(x: A): Unit } /* value future */ private class Value_Future[A](x: A) extends Future[A] { val peek: Option[Exn.Result[A]] = Some(Exn.Res(x)) def join_result: Exn.Result[A] = peek.get def cancel {} } /* task future via thread pool */ private class Task_Future[A](body: => A) extends Future[A] { private sealed abstract class Status private case object Ready extends Status private case class Running(thread: Thread) extends Status private case object Terminated extends Status private case class Finished(result: Exn.Result[A]) extends Status private val status = Synchronized[Status](Ready) def peek: Option[Exn.Result[A]] = status.value match { case Finished(result) => Some(result) case _ => None } private def try_run() { val do_run = status.change_result { case Ready => (true, Running(Thread.currentThread)) case st => (false, st) } if (do_run) { val result = Exn.capture(body) status.change(_ => Terminated) 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() }) def join_result: Exn.Result[A] = { try_run() status.guarded_access { case st @ Finished(result) => Some((result, st)) case _ => None } } def cancel = { status.change { case Ready => task.cancel(false); Finished(Exn.Exn(Exn.Interrupt())) case st @ Running(thread) => thread.interrupt; st case st => st } } } /* promise future */ private class Promise_Future[A] extends Promise[A] { private val state = Synchronized[Option[Exn.Result[A]]](None) def peek: Option[Exn.Result[A]] = state.value def join_result: Exn.Result[A] = state.guarded_access(st => if (st.isEmpty) None else Some((st.get, st))) def fulfill_result(result: Exn.Result[A]): Unit = state.change(st => if (st.isEmpty) Some(result) else throw new IllegalStateException) def fulfill(x: A): Unit = fulfill_result(Exn.Res(x)) def cancel: Unit = state.change(st => if (st.isEmpty) Some(Exn.Exn(Exn.Interrupt())) else st) } /* thread future */ private class Thread_Future[A]( name: String, group: ThreadGroup, pri: Int, daemon: Boolean, inherit_locals: Boolean, uninterruptible: Boolean, body: => A) extends Future[A] { private val result = Future.promise[A] private val thread = Isabelle_Thread.fork(name = name, group = group, pri = pri, daemon = daemon, inherit_locals = inherit_locals, uninterruptible = uninterruptible) { result.fulfill_result(Exn.capture(body)) } def peek: Option[Exn.Result[A]] = result.peek def join_result: Exn.Result[A] = result.join_result def cancel: Unit = thread.interrupt } diff --git a/src/Pure/Concurrent/isabelle_thread.scala b/src/Pure/Concurrent/isabelle_thread.scala --- a/src/Pure/Concurrent/isabelle_thread.scala +++ b/src/Pure/Concurrent/isabelle_thread.scala @@ -1,195 +1,195 @@ /* Title: Pure/Concurrent/isabelle_thread.scala Author: Makarius Isabelle-specific thread management. */ package isabelle import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue} object Isabelle_Thread { /* self-thread */ def self: Isabelle_Thread = Thread.currentThread match { case thread: Isabelle_Thread => thread case thread => error("Isabelle-specific thread required: " + thread) } def check_self: Boolean = Thread.currentThread.isInstanceOf[Isabelle_Thread] /* create threads */ private val counter = Counter.make() def make_name(name: String = "", base: String = "thread"): String = { val prefix = "Isabelle." val suffix = if (name.nonEmpty) name else base + counter() if (suffix.startsWith(prefix)) suffix else prefix + suffix } def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup lazy val worker_thread_group: ThreadGroup = new ThreadGroup(current_thread_group, "Isabelle worker") def create( main: Runnable, name: String = "", group: ThreadGroup = current_thread_group, pri: Int = Thread.NORM_PRIORITY, daemon: Boolean = false, inherit_locals: Boolean = false): Isabelle_Thread = { new Isabelle_Thread(main, name = make_name(name = name), group = group, pri = pri, daemon = daemon, inherit_locals = inherit_locals) } def fork( name: String = "", group: ThreadGroup = current_thread_group, pri: Int = Thread.NORM_PRIORITY, daemon: Boolean = false, inherit_locals: Boolean = false, uninterruptible: Boolean = false)(body: => Unit): Isabelle_Thread = { val main: Runnable = if (uninterruptible) { () => Isabelle_Thread.uninterruptible { body } } else { () => body } val thread = create(main, name = name, group = group, pri = pri, daemon = daemon, inherit_locals = inherit_locals) thread.start thread } /* thread pool */ def max_threads(): Int = { val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0 if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8 } lazy val pool: ThreadPoolExecutor = { val n = max_threads() val executor = new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable]) executor.setThreadFactory( create(_, name = make_name(base = "worker"), group = worker_thread_group)) executor } /* interrupt handlers */ object Interrupt_Handler { def apply(handle: Isabelle_Thread => Unit, name: String = "handler"): Interrupt_Handler = new Interrupt_Handler(handle, name) val interruptible: Interrupt_Handler = Interrupt_Handler(_.raise_interrupt, name = "interruptible") val uninterruptible: Interrupt_Handler = Interrupt_Handler(_.postpone_interrupt, name = "uninterruptible") } class Interrupt_Handler private(handle: Isabelle_Thread => Unit, name: String) extends Function[Isabelle_Thread, Unit] { def apply(thread: Isabelle_Thread) { handle(thread) } override def toString: String = name } def interrupt_handler[A](handler: Interrupt_Handler)(body: => A): A = if (handler == null) body else self.interrupt_handler(handler)(body) def interrupt_handler[A](handle: Isabelle_Thread => Unit)(body: => A): A = self.interrupt_handler(Interrupt_Handler(handle))(body) def interruptible[A](body: => A): A = interrupt_handler(Interrupt_Handler.interruptible)(body) def uninterruptible[A](body: => A): A = interrupt_handler(Interrupt_Handler.uninterruptible)(body) def try_uninterruptible[A](body: => A): A = if (check_self) interrupt_handler(Interrupt_Handler.uninterruptible)(body) else body } class Isabelle_Thread private(main: Runnable, name: String, group: ThreadGroup, pri: Int, daemon: Boolean, inherit_locals: Boolean) extends Thread(group, null, name, 0L, inherit_locals) { thread => thread.setPriority(pri) thread.setDaemon(daemon) override def run { main.run() } def is_self: Boolean = Thread.currentThread == thread /* interrupt state */ // synchronized, with concurrent changes private var interrupt_postponed: Boolean = false def clear_interrupt: Boolean = synchronized { val was_interrupted = isInterrupted || interrupt_postponed Exn.Interrupt.dispose() interrupt_postponed = false was_interrupted } def raise_interrupt: Unit = synchronized { interrupt_postponed = false super.interrupt() } def postpone_interrupt: Unit = synchronized { interrupt_postponed = true Exn.Interrupt.dispose() } /* interrupt handler */ // non-synchronized, only changed on self-thread @volatile private var handler = Isabelle_Thread.Interrupt_Handler.interruptible override def interrupt: Unit = handler(thread) def interrupt_handler[A](new_handler: Isabelle_Thread.Interrupt_Handler)(body: => A): A = if (new_handler == null) body else { - require(is_self) + require(is_self, "interrupt handler on other thread") val old_handler = handler handler = new_handler try { if (clear_interrupt) interrupt body } finally { handler = old_handler if (clear_interrupt) interrupt } } } diff --git a/src/Pure/GUI/gui_thread.scala b/src/Pure/GUI/gui_thread.scala --- a/src/Pure/GUI/gui_thread.scala +++ b/src/Pure/GUI/gui_thread.scala @@ -1,57 +1,57 @@ /* Title: Pure/GUI/gui_thread.scala Author: Makarius Evaluation within the GUI thread (for AWT/Swing). */ package isabelle import javax.swing.SwingUtilities object GUI_Thread { /* context check */ def assert[A](body: => A): A = { Predef.assert(SwingUtilities.isEventDispatchThread) body } def require[A](body: => A): A = { - Predef.require(SwingUtilities.isEventDispatchThread) + Predef.require(SwingUtilities.isEventDispatchThread, "GUI thread expected") body } /* event dispatch queue */ def now[A](body: => A): A = { if (SwingUtilities.isEventDispatchThread) body else { lazy val result = assert { Exn.capture(body) } SwingUtilities.invokeAndWait(() => result) Exn.release(result) } } def later(body: => Unit) { if (SwingUtilities.isEventDispatchThread) body else SwingUtilities.invokeLater(() => body) } def future[A](body: => A): Future[A] = { if (SwingUtilities.isEventDispatchThread) Future.value(body) else { val promise = Future.promise[A] later { promise.fulfill_result(Exn.capture(body)) } promise } } } diff --git a/src/Pure/General/date.scala b/src/Pure/General/date.scala --- a/src/Pure/General/date.scala +++ b/src/Pure/General/date.scala @@ -1,105 +1,105 @@ /* Title: Pure/General/date.scala Author: Makarius Date and time, with time zone. */ package isabelle import java.util.Locale import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId, OffsetDateTime} import java.time.format.{DateTimeFormatter, DateTimeParseException} import java.time.temporal.TemporalAccessor import scala.annotation.tailrec object Date { /* format */ object Format { def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format = { - require(fmts.nonEmpty) + require(fmts.nonEmpty, "no date formats") new Format { def apply(date: Date): String = fmts.head.format(date.rep) def parse(str: String): Date = new Date(ZonedDateTime.from(Formatter.try_variants(fmts, tune(str)))) } } def apply(pats: String*): Format = make(pats.toList.map(Date.Formatter.pattern)) val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx") val date: Format = Format("dd-MMM-uuuu") val time: Format = Format("HH:mm:ss") } abstract class Format private { def apply(date: Date): String def parse(str: String): Date def unapply(str: String): Option[Date] = try { Some(parse(str)) } catch { case _: DateTimeParseException => None } } object Formatter { def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat) def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] = pats.flatMap(pat => { val fmt = pattern(pat) if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale) }) @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String, last_exn: Option[DateTimeParseException] = None): TemporalAccessor = { fmts match { case Nil => throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0)) case fmt :: rest => try { ZonedDateTime.from(fmt.parse(str)) } catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) } } } } /* date operations */ def timezone_utc: ZoneId = ZoneId.of("UTC") def timezone_berlin: ZoneId = ZoneId.of("Europe/Berlin") def timezone(): ZoneId = ZoneId.systemDefault def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone)) def instant(t: Instant, zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.ofInstant(t, zone)) def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone) } sealed case class Date(rep: ZonedDateTime) { def midnight: Date = new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone)) def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone)) def unix_epoch: Long = rep.toEpochSecond def instant: Instant = Instant.from(rep) def time: Time = Time.instant(instant) def timezone: ZoneId = rep.getZone def format(fmt: Date.Format = Date.Format.default): String = fmt(this) override def toString: String = format() } diff --git a/src/Pure/General/scan.scala b/src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala +++ b/src/Pure/General/scan.scala @@ -1,512 +1,512 @@ /* Title: Pure/General/scan.scala Author: Makarius Efficient scanning of keywords and tokens. */ package isabelle import scala.annotation.tailrec import scala.collection.{IndexedSeq, Traversable, TraversableOnce} import scala.collection.immutable.PagedSeq import scala.util.matching.Regex import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader, CharSequenceReader} import scala.util.parsing.combinator.RegexParsers import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream} import java.net.URL object Scan { /** context of partial line-oriented scans **/ abstract class Line_Context case object Finished extends Line_Context case class Quoted(quote: String) extends Line_Context case object Verbatim extends Line_Context case class Cartouche(depth: Int) extends Line_Context case class Comment_Prefix(symbol: Symbol.Symbol) extends Line_Context case class Cartouche_Comment(depth: Int) extends Line_Context case class Comment(depth: Int) extends Line_Context /** parser combinators **/ object Parsers extends Parsers trait Parsers extends RegexParsers { override val whiteSpace: Regex = "".r /* optional termination */ def opt_term[T](p: => Parser[T]): Parser[Option[T]] = p ^^ (x => Some(x)) | """\z""".r ^^ (_ => None) /* repeated symbols */ def repeated(pred: Symbol.Symbol => Boolean, min_count: Int, max_count: Int): Parser[String] = new Parser[String] { def apply(in: Input) = { val start = in.offset val end = in.source.length val matcher = new Symbol.Matcher(in.source) var i = start var count = 0 var finished = false while (!finished && i < end && count < max_count) { val n = matcher(i, end) val sym = in.source.subSequence(i, i + n).toString if (pred(sym)) { i += n; count += 1 } else finished = true } if (count < min_count) Failure("bad input", in) else Success(in.source.subSequence(start, i).toString, in.drop(i - start)) } }.named("repeated") def one(pred: Symbol.Symbol => Boolean): Parser[String] = repeated(pred, 1, 1) def maybe(pred: Symbol.Symbol => Boolean): Parser[String] = repeated(pred, 0, 1) def many(pred: Symbol.Symbol => Boolean): Parser[String] = repeated(pred, 0, Integer.MAX_VALUE) def many1(pred: Symbol.Symbol => Boolean): Parser[String] = repeated(pred, 1, Integer.MAX_VALUE) /* character */ def character(pred: Char => Boolean): Symbol.Symbol => Boolean = (s: Symbol. Symbol) => s.length == 1 && pred(s.charAt(0)) /* quoted strings */ private def quoted_body(quote: Symbol.Symbol): Parser[String] = { rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" | ("""\\\d\d\d""".r ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString) } def quoted(quote: Symbol.Symbol): Parser[String] = { quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z } }.named("quoted") def quoted_content(quote: Symbol.Symbol, source: String): String = { - require(parseAll(quoted(quote), source).successful) + require(parseAll(quoted(quote), source).successful, "no quoted text") val body = source.substring(1, source.length - 1) if (body.exists(_ == '\\')) { val content = rep(many1(sym => sym != quote && sym != "\\") | "\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString })) parseAll(content ^^ (_.mkString), body).get } else body } def quoted_line(quote: Symbol.Symbol, ctxt: Line_Context): Parser[(String, Line_Context)] = { ctxt match { case Finished => quote ~ quoted_body(quote) ~ opt_term(quote) ^^ { case x ~ y ~ Some(z) => (x + y + z, Finished) case x ~ y ~ None => (x + y, Quoted(quote)) } case Quoted(q) if q == quote => quoted_body(quote) ~ opt_term(quote) ^^ { case x ~ Some(y) => (x + y, Finished) case x ~ None => (x, ctxt) } case _ => failure("") } }.named("quoted_line") def recover_quoted(quote: Symbol.Symbol): Parser[String] = quote ~ quoted_body(quote) ^^ { case x ~ y => x + y } /* verbatim text */ private def verbatim_body: Parser[String] = rep(many1(sym => sym != "*") | """\*(?!\})""".r) ^^ (_.mkString) def verbatim: Parser[String] = { "{*" ~ verbatim_body ~ "*}" ^^ { case x ~ y ~ z => x + y + z } }.named("verbatim") def verbatim_content(source: String): String = { - require(parseAll(verbatim, source).successful) + require(parseAll(verbatim, source).successful, "no verbatim text") source.substring(2, source.length - 2) } def verbatim_line(ctxt: Line_Context): Parser[(String, Line_Context)] = { ctxt match { case Finished => "{*" ~ verbatim_body ~ opt_term("*}") ^^ { case x ~ y ~ Some(z) => (x + y + z, Finished) case x ~ y ~ None => (x + y, Verbatim) } case Verbatim => verbatim_body ~ opt_term("*}") ^^ { case x ~ Some(y) => (x + y, Finished) case x ~ None => (x, Verbatim) } case _ => failure("") } }.named("verbatim_line") val recover_verbatim: Parser[String] = "{*" ~ verbatim_body ^^ { case x ~ y => x + y } /* nested text cartouches */ def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)] { - require(depth >= 0) + require(depth >= 0, "bad cartouche depth") def apply(in: Input) = { val start = in.offset val end = in.source.length val matcher = new Symbol.Matcher(in.source) var i = start var d = depth var finished = false while (!finished && i < end) { val n = matcher(i, end) val sym = in.source.subSequence(i, i + n).toString if (Symbol.is_open(sym)) { i += n; d += 1 } else if (Symbol.is_close(sym) && d > 0) { i += n; d -= 1; if (d == 0) finished = true } else if (d > 0) i += n else finished = true } if (i == start) Failure("bad input", in) else Success((in.source.subSequence(start, i).toString, d), in.drop(i - start)) } }.named("cartouche_depth") def cartouche: Parser[String] = cartouche_depth(0) ^? { case (x, d) if d == 0 => x } def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] = { def cartouche_context(d: Int): Line_Context = if (d == 0) Finished else Cartouche(d) ctxt match { case Finished => cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) } case Cartouche(depth) => cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) } case _ => failure("") } } val recover_cartouche: Parser[String] = cartouche_depth(0) ^^ (_._1) def cartouche_content(source: String): String = { def err(): Nothing = error("Malformed text cartouche: " + quote(source)) val source1 = Library.try_unprefix(Symbol.open_decoded, source) orElse Library.try_unprefix(Symbol.open, source) getOrElse err() Library.try_unsuffix(Symbol.close_decoded, source1) orElse Library.try_unsuffix(Symbol.close, source1) getOrElse err() } /* nested comments */ private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)] { - require(depth >= 0) + require(depth >= 0, "bad comment depth") val comment_text: Parser[List[String]] = rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r) def apply(in: Input) = { var rest = in def try_parse[A](p: Parser[A]): Boolean = { parse(p ^^^ (()), rest) match { case Success(_, next) => { rest = next; true } case _ => false } } var d = depth var finished = false while (!finished) { if (try_parse("(*")) d += 1 else if (d > 0 && try_parse("*)")) { d -= 1; if (d == 0) finished = true } else if (d == 0 || !try_parse(comment_text)) finished = true } if (in.offset < rest.offset) Success((in.source.subSequence(in.offset, rest.offset).toString, d), rest) else Failure("comment expected", in) } }.named("comment_depth") def comment: Parser[String] = comment_depth(0) ^? { case (x, d) if d == 0 => x } def comment_line(ctxt: Line_Context): Parser[(String, Line_Context)] = { val depth = ctxt match { case Finished => 0 case Comment(d) => d case _ => -1 } if (depth >= 0) comment_depth(depth) ^^ { case (x, 0) => (x, Finished) case (x, d) => (x, Comment(d)) } else failure("") } val recover_comment: Parser[String] = comment_depth(0) ^^ (_._1) def comment_content(source: String): String = { - require(parseAll(comment, source).successful) + require(parseAll(comment, source).successful, "no comment") source.substring(2, source.length - 2) } /* keyword */ def literal(lexicon: Lexicon): Parser[String] = new Parser[String] { def apply(in: Input) = { val result = lexicon.scan(in) if (result.isEmpty) Failure("keyword expected", in) else Success(result, in.drop(result.length)) } }.named("keyword") } /** Lexicon -- position tree **/ object Lexicon { /* representation */ private sealed case class Tree(branches: Map[Char, (String, Tree)]) private val empty_tree = Tree(Map()) val empty: Lexicon = new Lexicon(empty_tree) def apply(elems: String*): Lexicon = empty ++ elems } final class Lexicon private(rep: Lexicon.Tree) { /* 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) }) private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] = { val len = str.length @tailrec def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] = { if (i < len) { tree.branches.get(str.charAt(i)) match { case Some((s, tr)) => look(tr, s.nonEmpty, i + 1) case None => None } } else Some(tip, tree) } look(rep, false, 0) } def completions(str: CharSequence): List[String] = lookup(str) match { case Some((true, tree)) => dest(tree, List(str.toString)) case Some((false, tree)) => dest(tree, Nil) case None => Nil } /* pseudo Set methods */ def raw_iterator: Iterator[String] = dest(rep, Nil).iterator def iterator: Iterator[String] = dest(rep, Nil).sorted.iterator override def toString: String = iterator.mkString("Lexicon(", ", ", ")") def is_empty: Boolean = rep.branches.isEmpty def contains(elem: String): Boolean = lookup(elem) match { case Some((tip, _)) => tip case _ => false } /* build lexicon */ def + (elem: String): Lexicon = if (contains(elem)) this else { val len = elem.length def extend(tree: Lexicon.Tree, i: Int): Lexicon.Tree = if (i < len) { val c = elem.charAt(i) val end = (i + 1 == len) tree.branches.get(c) match { case Some((s, tr)) => Lexicon.Tree(tree.branches + (c -> (if (end) elem else s, extend(tr, i + 1)))) case None => Lexicon.Tree(tree.branches + (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1)))) } } else tree new Lexicon(extend(rep, 0)) } def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _) def ++ (other: Lexicon): Lexicon = if (this eq other) this else if (is_empty) other else this ++ other.raw_iterator def -- (remove: Traversable[String]): Lexicon = if (remove.exists(contains)) Lexicon.empty ++ iterator.filterNot(a => remove.exists(b => a == b)) else this /* scan */ def scan(in: Reader[Char]): String = { val source = in.source val offset = in.offset val len = source.length - offset @tailrec def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String = { if (i < len) { tree.branches.get(source.charAt(offset + i)) match { case Some((s, tr)) => scan_tree(tr, if (s.isEmpty) result else s, i + 1) case None => result } } else result } scan_tree(rep, "", 0) } } /** read stream without decoding: efficient length operation **/ private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int) extends CharSequence { def charAt(i: Int): Char = if (0 <= i && i < length) seq(start + i) else throw new IndexOutOfBoundsException def length: Int = end - start // avoid expensive seq.length def subSequence(i: Int, j: Int): CharSequence = if (0 <= i && i <= j && j <= length) new Restricted_Seq(seq, start + i, start + j) else throw new IndexOutOfBoundsException override def toString: String = { val buf = new StringBuilder(length) for (offset <- start until end) buf.append(seq(offset)) buf.toString } } abstract class Byte_Reader extends Reader[Char] with AutoCloseable private def make_byte_reader(stream: InputStream, stream_length: Int): Byte_Reader = { val buffered_stream = new BufferedInputStream(stream) val seq = new PagedSeq( (buf: Array[Char], offset: Int, length: Int) => { var i = 0 var c = 0 var eof = false while (!eof && i < length) { c = buffered_stream.read if (c == -1) eof = true else { buf(offset + i) = c.toChar; i += 1 } } if (i > 0) i else -1 }) val restricted_seq = new Restricted_Seq(seq, 0, stream_length) class Paged_Reader(override val offset: Int) extends Byte_Reader { override lazy val source: CharSequence = restricted_seq def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\u001a' def rest: Paged_Reader = if (seq.isDefinedAt(offset)) new Paged_Reader(offset + 1) else this 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 { buffered_stream.close } } new Paged_Reader(0) } def byte_reader(file: JFile): Byte_Reader = make_byte_reader(new FileInputStream(file), file.length.toInt) def byte_reader(url: URL): Byte_Reader = { val connection = url.openConnection val stream = connection.getInputStream val stream_length = connection.getContentLength make_byte_reader(stream, stream_length) } def reader_is_utf8(reader: Reader[Char]): Boolean = reader.isInstanceOf[Byte_Reader] def reader_decode_utf8(is_utf8: Boolean, s: String): String = if (is_utf8) UTF8.decode_permissive(s) else s def reader_decode_utf8(reader: Reader[Char], s: String): String = reader_decode_utf8(reader_is_utf8(reader), s) /* plain text reader */ def char_reader(text: CharSequence): CharSequenceReader = new CharSequenceReader(text) } diff --git a/src/Pure/General/symbol.scala b/src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala +++ b/src/Pure/General/symbol.scala @@ -1,668 +1,668 @@ /* Title: Pure/General/symbol.scala Author: Makarius Isabelle text symbols. */ package isabelle import scala.collection.mutable import scala.util.matching.Regex import scala.annotation.tailrec object Symbol { type Symbol = String // counting Isabelle symbols, starting from 1 type Offset = Text.Offset type Range = Text.Range /* spaces */ val space_char = ' ' val space = " " private val static_spaces = space * 4000 def spaces(n: Int): String = { - require(n >= 0) + require(n >= 0, "negative spaces") if (n < static_spaces.length) static_spaces.substring(0, n) else space * n } /* ASCII characters */ def is_ascii_printable(c: Char): Boolean = space_char <= c && c <= '~' def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9' def is_ascii_hex(c: Char): Boolean = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f' def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\'' def is_ascii_blank(c: Char): Boolean = " \t\n\u000b\f\r".contains(c) def is_ascii_line_terminator(c: Char): Boolean = "\r\n".contains(c) def is_ascii_letdig(c: Char): Boolean = is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c) def is_ascii_identifier(s: String): Boolean = s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig) def ascii(c: Char): Symbol = { if (c > 127) error("Non-ASCII character: " + quote(c.toString)) else char_symbols(c.toInt) } def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128 /* symbol matching */ private val symbol_total = new Regex("""(?xs) [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""") private def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || Character.isHighSurrogate(c)) def is_malformed(s: Symbol): Boolean = s.length match { case 1 => val c = s(0) Character.isHighSurrogate(c) || Character.isLowSurrogate(c) || c == '\ufffd' case 2 => val c1 = s(0) val c2 = s(1) !(c1 == '\r' && c2 == '\n' || Character.isSurrogatePair(c1, c2)) case _ => !s.endsWith(">") || s == "\\<>" || s == "\\<^>" } def is_newline(s: Symbol): Boolean = s == "\n" || s == "\r" || s == "\r\n" class Matcher(text: CharSequence) { private val matcher = symbol_total.pattern.matcher(text) def apply(start: Int, end: Int): Int = { - require(0 <= start && start < end && end <= text.length) + require(0 <= start && start < end && end <= text.length, "bad matcher range") if (is_plain(text.charAt(start))) 1 else { matcher.region(start, end).lookingAt matcher.group.length } } } /* iterator */ private val char_symbols: Array[Symbol] = (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray def iterator(text: CharSequence): Iterator[Symbol] = new Iterator[Symbol] { private val matcher = new Matcher(text) private var i = 0 def hasNext: Boolean = i < text.length def next: Symbol = { val n = matcher(i, text.length) val s = if (n == 0) "" else if (n == 1) { val c = text.charAt(i) if (c < char_symbols.length) char_symbols(c) else text.subSequence(i, i + n).toString } else text.subSequence(i, i + n).toString i += n s } } def explode(text: CharSequence): List[Symbol] = iterator(text).toList def length(text: CharSequence): Int = iterator(text).length def trim_blanks(text: CharSequence): String = Library.trim(is_blank, explode(text)).mkString def all_blank(str: String): Boolean = iterator(str).forall(is_blank) def trim_blank_lines(text: String): String = cat_lines(split_lines(text).dropWhile(all_blank).reverse.dropWhile(all_blank).reverse) /* decoding offsets */ object Index { private sealed case class Entry(chr: Int, sym: Int) val empty: Index = new Index(Nil) def apply(text: CharSequence): Index = { val matcher = new Matcher(text) val buf = new mutable.ListBuffer[Entry] var chr = 0 var sym = 0 while (chr < text.length) { val n = matcher(chr, text.length) chr += n sym += 1 if (n > 1) buf += Entry(chr, sym) } if (buf.isEmpty) empty else new Index(buf.toList) } } final class Index private(entries: List[Index.Entry]) { private val hash: Int = entries.hashCode private val index: Array[Index.Entry] = entries.toArray def decode(symbol_offset: Offset): Text.Offset = { val sym = symbol_offset - 1 val end = index.length @tailrec def bisect(a: Int, b: Int): Int = { if (a < b) { val c = (a + b) / 2 if (sym < index(c).sym) bisect(a, c) else if (c + 1 == end || sym < index(c + 1).sym) c else bisect(c + 1, b) } else -1 } val i = bisect(0, end) if (i < 0) sym else index(i).chr + sym - index(i).sym } def decode(symbol_range: Range): Text.Range = symbol_range.map(decode) override def hashCode: Int = hash override def equals(that: Any): Boolean = that match { case other: Index => index.sameElements(other.index) case _ => false } } /* symbolic text chunks -- without actual text */ object Text_Chunk { sealed abstract class Name case object Default extends Name case class Id(id: Document_ID.Generic) extends Name case class File(name: String) extends Name def apply(text: CharSequence): Text_Chunk = new Text_Chunk(Text.Range(0, text.length), Index(text)) } final class Text_Chunk private(val range: Text.Range, private val index: Index) { override def hashCode: Int = (range, index).hashCode override def equals(that: Any): Boolean = that match { case other: Text_Chunk => range == other.range && index == other.index case _ => false } override def toString: String = "Text_Chunk" + range.toString def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset) def decode(symbol_range: Range): Text.Range = index.decode(symbol_range) def incorporate(symbol_range: Range): Option[Text.Range] = { def in(r: Range): Option[Text.Range] = range.try_restrict(decode(r)) match { case Some(r1) if !r1.is_singularity => Some(r1) case _ => None } in(symbol_range) orElse in(symbol_range - 1) } } /* recoding text */ private class Recoder(list: List[(String, String)]) { private val (min, max) = { var min = '\uffff' var max = '\u0000' for ((x, _) <- list) { val c = x(0) if (c < min) min = c if (c > max) max = c } (min, max) } private val table = { var tab = Map[String, String]() for ((x, y) <- list) { tab.get(x) match { case None => tab += (x -> y) case Some(z) => error("Duplicate symbol mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z)) } } tab } def recode(text: String): String = { val len = text.length val matcher = symbol_total.pattern.matcher(text) val result = new StringBuilder(len) var i = 0 while (i < len) { val c = text(i) if (min <= c && c <= max) { matcher.region(i, len).lookingAt val x = matcher.group result.append(table.getOrElse(x, x)) i = matcher.end } else { result.append(c); i += 1 } } result.toString } } /** symbol interpretation **/ val ARGUMENT_CARTOUCHE = "cartouche" val ARGUMENT_SPACE_CARTOUCHE = "space_cartouche" private lazy val symbols = { val contents = for (path <- Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS")) if path.is_file) yield (File.read(path)) new Interpretation(cat_lines(contents)) } private class Interpretation(symbols_spec: String) { /* read symbols */ private val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """) private val Key = new Regex("""(?xs) (.+): """) private def read_decl(decl: String): (Symbol, Properties.T) = { def err() = error("Bad symbol declaration: " + decl) def read_props(props: List[String]): Properties.T = { props match { case Nil => Nil case _ :: Nil => err() case Key(x) :: y :: rest => (x -> y.replace('\u2423', ' ')) :: read_props(rest) case _ => err() } } decl.split("\\s+").toList match { case sym :: props if sym.length > 1 && !is_malformed(sym) => (sym, read_props(props)) case _ => err() } } 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 case ((list, known), decl) => val (sym, props) = read_decl(decl) if (known(sym)) (list, known) else ((sym, props) :: list, known + sym) })._1 /* basic properties */ val properties: Map[Symbol, Properties.T] = Map(symbols: _*) val names: Map[Symbol, (String, String)] = { val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""") val Argument = new Properties.String("argument") def argument(sym: Symbol, props: Properties.T): String = props match { case Argument(arg) => if (arg == ARGUMENT_CARTOUCHE || arg == ARGUMENT_SPACE_CARTOUCHE) arg else error("Bad argument: " + quote(arg) + " for symbol " + quote(sym)) case _ => "" } Map((for ((sym @ Name(a), props) <- symbols) yield sym -> (a, argument(sym, props))): _*) } val groups: List[(String, List[Symbol])] = symbols.flatMap({ case (sym, props) => val gs = for (("group", g) <- props) yield g if (gs.isEmpty) List(sym -> "unsorted") else gs.map(sym -> _) }).groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) }) .sortBy(_._1) val abbrevs: Multi_Map[Symbol, String] = Multi_Map(( for { (sym, props) <- symbols ("abbrev", a) <- props.reverse } yield sym -> a): _*) val codes: List[(Symbol, Int)] = { val Code = new Properties.String("code") for { (sym, props) <- symbols code <- props match { case Code(s) => try { Some(Integer.decode(s).intValue) } catch { case _: NumberFormatException => error("Bad code for symbol " + sym) } case _ => None } } yield { if (code < 128) error("Illegal ASCII code for symbol " + sym) else (sym, code) } } /* recoding */ private val (decoder, encoder) = { val mapping = for ((sym, code) <- codes) yield (sym, new String(Character.toChars(code))) (new Recoder(mapping), new Recoder(for ((x, y) <- mapping) yield (y, x))) } def decode(text: String): String = decoder.recode(text) def encode(text: String): String = encoder.recode(text) private def recode_set(elems: String*): Set[String] = { val content = elems.toList Set((content ::: content.map(decode)): _*) } private def recode_map[A](elems: (String, A)*): Map[String, A] = { val content = elems.toList Map((content ::: content.map({ case (sym, a) => (decode(sym), a) })): _*) } /* user fonts */ private val Font = new Properties.String("font") val fonts: Map[Symbol, String] = recode_map((for ((sym, Font(font)) <- symbols) yield sym -> font): _*) val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList val font_index: Map[String, Int] = Map((font_names zip font_names.indices.toList): _*) /* classification */ val letters: Set[String] = recode_set( "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\

", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\

", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\
", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\") val blanks: Set[String] = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n") val sym_chars = Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~") val symbolic: Set[String] = recode_set((for {(sym, _) <- symbols; if raw_symbolic(sym)} yield sym): _*) /* misc symbols */ val newline_decoded = decode(newline) val comment_decoded = decode(comment) val cancel_decoded = decode(cancel) val latex_decoded = decode(latex) val marker_decoded = decode(marker) val open_decoded = decode(open) val close_decoded = decode(close) /* control symbols */ val control_decoded: Set[Symbol] = Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*) val sub_decoded = decode(sub) val sup_decoded = decode(sup) val bold_decoded = decode(bold) val emph_decoded = decode(emph) val bsub_decoded = decode(bsub) val esub_decoded = decode(esub) val bsup_decoded = decode(bsup) val esup_decoded = decode(esup) } /* tables */ def properties: Map[Symbol, Properties.T] = symbols.properties def names: Map[Symbol, (String, String)] = symbols.names def groups: List[(String, List[Symbol])] = symbols.groups def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs def codes: List[(Symbol, Int)] = symbols.codes def groups_code: List[(String, List[Symbol])] = { val has_code = codes.iterator.map(_._1).toSet groups.flatMap({ case (group, symbols) => val symbols1 = symbols.filter(has_code) if (symbols1.isEmpty) None else Some((group, symbols1)) }) } lazy val is_code: Int => Boolean = codes.map(_._2).toSet def decode(text: String): String = symbols.decode(text) def encode(text: String): String = symbols.encode(text) def decode_yxml(text: String, cache: XML.Cache = XML.Cache.none): XML.Body = YXML.parse_body(decode(text), cache = cache) def decode_yxml_failsafe(text: String, cache: XML.Cache = XML.Cache.none): XML.Body = YXML.parse_body_failsafe(decode(text), cache = cache) def encode_yxml(body: XML.Body): String = encode(YXML.string_of_body(body)) def decode_strict(text: String): String = { val decoded = decode(text) if (encode(decoded) == text) decoded else { val bad = new mutable.ListBuffer[Symbol] for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s)) bad += s error("Bad Unicode symbols in text: " + commas_quote(bad)) } } def output(unicode_symbols: Boolean, text: String): String = if (unicode_symbols) Symbol.decode(text) else Symbol.encode(text) def fonts: Map[Symbol, String] = symbols.fonts def font_names: List[String] = symbols.font_names def font_index: Map[String, Int] = symbols.font_index def lookup_font(sym: Symbol): Option[Int] = symbols.fonts.get(sym).map(font_index(_)) /* classification */ def is_letter(sym: Symbol): Boolean = symbols.letters.contains(sym) def is_digit(sym: Symbol): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9' def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'" def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym) def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym) /* symbolic newline */ val newline: Symbol = "\\" def newline_decoded: Symbol = symbols.newline_decoded def print_newlines(str: String): String = if (str.contains('\n')) (for (s <- iterator(str)) yield { if (s == "\n") newline_decoded else s }).mkString else str /* formal comments */ val comment: Symbol = "\\" val cancel: Symbol = "\\<^cancel>" val latex: Symbol = "\\<^latex>" val marker: Symbol = "\\<^marker>" def comment_decoded: Symbol = symbols.comment_decoded def cancel_decoded: Symbol = symbols.cancel_decoded def latex_decoded: Symbol = symbols.latex_decoded def marker_decoded: Symbol = symbols.marker_decoded /* cartouches */ val open: Symbol = "\\" val close: Symbol = "\\" def open_decoded: Symbol = symbols.open_decoded def close_decoded: Symbol = symbols.close_decoded def is_open(sym: Symbol): Boolean = sym == open_decoded || sym == open def is_close(sym: Symbol): Boolean = sym == close_decoded || sym == close def cartouche(s: String): String = open + s + close def cartouche_decoded(s: String): String = open_decoded + s + close_decoded /* symbols for symbolic identifiers */ private def raw_symbolic(sym: Symbol): Boolean = sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^") def is_symbolic(sym: Symbol): Boolean = !is_open(sym) && !is_close(sym) && (raw_symbolic(sym) || symbols.symbolic.contains(sym)) def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym) /* control symbols */ val control_prefix = "\\<^" val control_suffix = ">" def control_name(sym: Symbol): Option[String] = if (is_control_encoded(sym)) Some(sym.substring(control_prefix.length, sym.length - control_suffix.length)) else None def is_control_encoded(sym: Symbol): Boolean = sym.startsWith(control_prefix) && sym.endsWith(control_suffix) def is_control(sym: Symbol): Boolean = is_control_encoded(sym) || symbols.control_decoded.contains(sym) def is_controllable(sym: Symbol): Boolean = !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym) && sym != "\"" val sub = "\\<^sub>" val sup = "\\<^sup>" val bold = "\\<^bold>" val emph = "\\<^emph>" val bsub = "\\<^bsub>" val esub = "\\<^esub>" val bsup = "\\<^bsup>" val esup = "\\<^esup>" def sub_decoded: Symbol = symbols.sub_decoded def sup_decoded: Symbol = symbols.sup_decoded def bold_decoded: Symbol = symbols.bold_decoded def emph_decoded: Symbol = symbols.emph_decoded def bsub_decoded: Symbol = symbols.bsub_decoded def esub_decoded: Symbol = symbols.esub_decoded def bsup_decoded: Symbol = symbols.bsup_decoded def esup_decoded: Symbol = symbols.esup_decoded /* metric */ def is_printable(sym: Symbol): Boolean = if (is_ascii(sym)) is_ascii_printable(sym(0)) else !is_control(sym) object Metric extends Pretty.Metric { val unit = 1.0 def apply(str: String): Double = (for (s <- iterator(str)) yield { val sym = encode(s) if (sym.startsWith("\\ String, buffer: Array[Byte], start: Int, end: Int) extends CharSequence { def length: Int = end - start def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char] def subSequence(i: Int, j: Int): CharSequence = new Decode_Chars(decode, buffer, start + i, start + j) // toString with adhoc decoding: abuse of CharSequence interface override def toString: String = decode(decode_permissive(this)) } def decode_chars(decode: String => String, buffer: Array[Byte], start: Int, end: Int): CharSequence = { - require(0 <= start && start <= end && end <= buffer.length) + require(0 <= start && start <= end && end <= buffer.length, "bad decode range") new Decode_Chars(decode, buffer, start, end) } } diff --git a/src/Pure/Isar/outer_syntax.scala b/src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala +++ b/src/Pure/Isar/outer_syntax.scala @@ -1,210 +1,210 @@ /* Title: Pure/Isar/outer_syntax.scala Author: Makarius Isabelle/Isar outer syntax. */ package isabelle import scala.collection.mutable object Outer_Syntax { /* syntax */ val empty: Outer_Syntax = new Outer_Syntax() def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _) /* string literals */ def quote_string(str: String): String = { val result = new StringBuilder(str.length + 10) result += '"' for (s <- Symbol.iterator(str)) { if (s.length == 1) { val c = s(0) if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') { result += '\\' if (c < 10) result += '0' if (c < 100) result += '0' result ++= c.asInstanceOf[Int].toString } else result += c } else result ++= s } result += '"' result.toString } } final class Outer_Syntax private( val keywords: Keyword.Keywords = Keyword.Keywords.empty, val rev_abbrevs: Thy_Header.Abbrevs = Nil, val language_context: Completion.Language_Context = Completion.Language_Context.outer, val has_tokens: Boolean = true) { /** syntax content **/ override def toString: String = keywords.toString /* keywords */ def + (name: String, kind: String = "", load_command: String = ""): Outer_Syntax = new Outer_Syntax( keywords + (name, kind, load_command), rev_abbrevs, language_context, has_tokens = true) def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = (this /: keywords) { case (syntax, (name, spec)) => syntax + (Symbol.decode(name), spec.kind, spec.load_command) + (Symbol.encode(name), spec.kind, spec.load_command) } /* abbrevs */ def abbrevs: Thy_Header.Abbrevs = rev_abbrevs.reverse def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax = if (new_abbrevs.isEmpty) this else { val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs new Outer_Syntax(keywords, rev_abbrevs1, language_context, has_tokens) } /* completion */ private lazy val completion: Completion = { val completion_keywords = (keywords.minor.iterator ++ keywords.major.iterator).toList val completion_abbrevs = completion_keywords.flatMap(name => (if (Keyword.theory_block.contains(keywords.kinds(name))) List((name, name + "\nbegin\n\u0007\nend")) else Nil) ::: (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil)) ::: abbrevs.flatMap( { case (a, b) => val a1 = Symbol.decode(a) val a2 = Symbol.encode(a) val b1 = Symbol.decode(b) List((a1, b1), (a2, b1)) }) Completion.make(completion_keywords, completion_abbrevs) } def complete( history: Completion.History, unicode: Boolean, explicit: Boolean, start: Text.Offset, text: CharSequence, caret: Int, context: Completion.Language_Context): Option[Completion.Result] = { completion.complete(history, unicode, explicit, start, text, caret, context) } /* build */ def + (header: Document.Node.Header): Outer_Syntax = add_keywords(header.keywords).add_abbrevs(header.abbrevs) def ++ (other: Outer_Syntax): Outer_Syntax = if (this eq other) this else if (this eq Outer_Syntax.empty) other else { val keywords1 = keywords ++ other.keywords val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs) if ((keywords eq keywords1) && (rev_abbrevs eq rev_abbrevs1)) this else new Outer_Syntax(keywords1, rev_abbrevs1, language_context, has_tokens) } /* load commands */ def load_command(name: String): Option[String] = keywords.load_commands.get(name) def has_load_commands(text: String): Boolean = keywords.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) /* language context */ def set_language_context(context: Completion.Language_Context): Outer_Syntax = new Outer_Syntax(keywords, rev_abbrevs, context, has_tokens) def no_tokens: Outer_Syntax = { - require(keywords.is_empty) + require(keywords.is_empty, "bad syntax keywords") new Outer_Syntax( rev_abbrevs = rev_abbrevs, language_context = language_context, has_tokens = false) } /** parsing **/ /* command spans */ def parse_spans(toks: List[Token]): List[Command_Span.Span] = { val result = new mutable.ListBuffer[Command_Span.Span] val content = new mutable.ListBuffer[Token] val ignored = new mutable.ListBuffer[Token] def ship(content: List[Token]) { val kind = if (content.forall(_.is_ignored)) Command_Span.Ignored_Span else if (content.exists(_.is_error)) Command_Span.Malformed_Span else content.find(_.is_command) match { case None => Command_Span.Malformed_Span case Some(cmd) => val name = cmd.source val offset = (0 /: content.takeWhile(_ != cmd)) { 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)) } result += Command_Span.Span(kind, content) } def flush() { if (content.nonEmpty) { ship(content.toList); content.clear } if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear } } for (tok <- toks) { if (tok.is_ignored) ignored += tok else if (keywords.is_before_command(tok) || tok.is_command && (!content.exists(keywords.is_before_command) || content.exists(_.is_command))) { flush(); content += tok } else { content ++= ignored; ignored.clear; content += tok } } flush() result.toList } def parse_spans(input: CharSequence): List[Command_Span.Span] = parse_spans(Token.explode(keywords, input)) } diff --git a/src/Pure/ML/ml_statistics.scala b/src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala +++ b/src/Pure/ML/ml_statistics.scala @@ -1,324 +1,324 @@ /* Title: Pure/ML/ml_statistics.scala Author: Makarius ML runtime statistics. */ package isabelle import scala.annotation.tailrec import scala.collection.mutable import scala.collection.immutable.{SortedSet, SortedMap} import scala.swing.{Frame, Component} import org.jfree.data.xy.{XYSeries, XYSeriesCollection} import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} import org.jfree.chart.plot.PlotOrientation object ML_Statistics { /* properties */ val Now = new Properties.Double("now") def now(props: Properties.T): Double = Now.unapply(props).get /* memory status */ val Heap_Size = new Properties.Long("size_heap") val Heap_Free = new Properties.Long("size_heap_free_last_GC") val GC_Percent = new Properties.Int("GC_percent") sealed case class Memory_Status(heap_size: Long, heap_free: Long, gc_percent: Int) { def heap_used: Long = (heap_size - heap_free) max 0 def heap_used_fraction: Double = if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size def gc_progress: Option[Double] = if (1 <= gc_percent && gc_percent <= 100) Some((gc_percent - 1) * 0.01) else None } def memory_status(props: Properties.T): Memory_Status = { val heap_size = Heap_Size.get(props) val heap_free = Heap_Free.get(props) val gc_percent = GC_Percent.get(props) Memory_Status(heap_size, heap_free, gc_percent) } /* monitor process */ def monitor(pid: Long, stats_dir: String = "", delay: Time = Time.seconds(0.5), consume: Properties.T => Unit = Console.println) { def progress_stdout(line: String) { val props = Library.space_explode(',', line).flatMap((entry: String) => Library.space_explode('=', entry) match { case List(a, b) => Some((a, b)) case _ => None }) if (props.nonEmpty) consume(props) } val env_prefix = if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n" Bash.process(env_prefix + "exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " + ML_Syntax.print_double(delay.seconds)), cwd = Path.explode("~~").file) .result(progress_stdout = progress_stdout, strict = false).check } /* protocol handler */ class Handler extends Session.Protocol_Handler { private var session: Session = null private var monitoring: Future[Unit] = Future.value(()) override def init(session: Session): Unit = synchronized { this.session = session } override def exit(): Unit = synchronized { session = null monitoring.cancel } private def consume(props: Properties.T): Unit = synchronized { if (session != null) { val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics())) session.runtime_statistics.post(Session.Runtime_Statistics(props1)) } } private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.ML_Statistics(pid, stats_dir) => monitoring = Future.thread("ML_statistics") { monitor(pid, stats_dir = stats_dir, consume = consume) } true case _ => false } } override val functions = List(Markup.ML_Statistics.name -> ml_statistics) } /* memory fields (mega bytes) */ def mem_print(x: Long): Option[String] = if (x == 0L) None else Some(x.toString + " M") def mem_scale(x: Long): Long = x / 1024 / 1024 def mem_field_scale(name: String, x: Double): Double = if (heap_fields._2.contains(name) || program_fields._2.contains(name)) mem_scale(x.toLong).toDouble else x val CODE_SIZE = "size_code" val STACK_SIZE = "size_stacks" val HEAP_SIZE = "size_heap" /* standard fields */ type Fields = (String, List[String]) val tasks_fields: Fields = ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent", "tasks_total")) val workers_fields: Fields = ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) val GC_fields: Fields = ("GCs", List("partial_GCs", "full_GCs", "share_passes")) val heap_fields: Fields = ("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free", "size_heap_free_last_full_GC", "size_heap_free_last_GC")) val program_fields: Fields = ("Program", List("size_code", "size_stacks")) val threads_fields: Fields = ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) val time_fields: Fields = ("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC")) val speed_fields: Fields = ("Speed", List("speed_CPU", "speed_GC")) private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC") val java_heap_fields: Fields = ("Java heap", List("java_heap_size", "java_heap_used")) val java_thread_fields: Fields = ("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active")) val main_fields: List[Fields] = List(heap_fields, tasks_fields, workers_fields) val other_fields: List[Fields] = List(threads_fields, GC_fields, program_fields, time_fields, speed_fields, java_heap_fields, java_thread_fields) val all_fields: List[Fields] = main_fields ::: other_fields /* content interpretation */ final case class Entry(time: Double, data: Map[String, Double]) { def get(field: String): Double = data.getOrElse(field, 0.0) } val empty: ML_Statistics = apply(Nil) def apply(ml_statistics0: List[Properties.T], heading: String = "", domain: String => Boolean = (key: String) => true): ML_Statistics = { - require(ml_statistics0.forall(props => Now.unapply(props).isDefined)) + require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field") val ml_statistics = ml_statistics0.sortBy(now) val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head) val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start val fields = SortedSet.empty[String] ++ (for { props <- ml_statistics.iterator (x, _) <- props.iterator if x != Now.name && domain(x) } yield x) val content = { var last_edge = Map.empty[String, (Double, Double, Double)] val result = new mutable.ListBuffer[ML_Statistics.Entry] for (props <- ml_statistics) { val time = now(props) - time_start // rising edges -- relative speed val speeds = (for { (key, value) <- props.iterator key1 <- time_speed.get(key) if domain(key1) } yield { val (x0, y0, s0) = last_edge.getOrElse(key, (0.0, 0.0, 0.0)) val x1 = time val y1 = java.lang.Double.parseDouble(value) val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0) if (y1 > y0) { last_edge += (key -> (x1, y1, s1)) (key1, s1.toString) } else (key1, s0.toString) }).toList val data = SortedMap.empty[String, Double] ++ (for { (x, y) <- props.iterator ++ speeds.iterator if x != Now.name && domain(x) z = java.lang.Double.parseDouble(y) if z != 0.0 } yield { (x.intern, mem_field_scale(x, z)) }) result += ML_Statistics.Entry(time, data) } result.toList } new ML_Statistics(heading, fields, content, time_start, duration) } } final class ML_Statistics private( val heading: String, val fields: Set[String], val content: List[ML_Statistics.Entry], val time_start: Double, val duration: Double) { /* content */ def maximum(field: String): Double = (0.0 /: content)({ case (m, e) => m max e.get(field) }) def average(field: String): Double = { @tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double = list match { case Nil => acc case e :: es => val t = e.time sum(t, es, (t - t0) * e.get(field) + acc) } content match { case Nil => 0.0 case List(e) => e.get(field) case e :: es => sum(e.time, es, 0.0) / duration } } /* charts */ def update_data(data: XYSeriesCollection, selected_fields: List[String]) { data.removeAllSeries for (field <- selected_fields) { val series = new XYSeries(field) content.foreach(entry => series.add(entry.time, entry.get(field))) data.addSeries(series) } } def chart(title: String, selected_fields: List[String]): JFreeChart = { val data = new XYSeriesCollection update_data(data, selected_fields) ChartFactory.createXYLineChart(title, "time", "value", data, PlotOrientation.VERTICAL, true, true, true) } def chart(fields: ML_Statistics.Fields): JFreeChart = chart(fields._1, fields._2) def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit = fields.map(chart).foreach(c => GUI_Thread.later { new Frame { iconImage = GUI.isabelle_image() title = heading contents = Component.wrap(new ChartPanel(c)) visible = true } }) } diff --git a/src/Pure/PIDE/command.scala b/src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala +++ b/src/Pure/PIDE/command.scala @@ -1,651 +1,651 @@ /* Title: Pure/PIDE/command.scala Author: Fabian Immler, TU Munich Author: Makarius Prover commands with accumulated results from execution. */ package isabelle import scala.collection.immutable.SortedMap object Command { /* blobs */ object Blob { def read_file(name: Document.Node.Name, src_path: Path): Blob = { val bytes = Bytes.read(name.path) val chunk = Symbol.Text_Chunk(bytes.text) Blob(name, src_path, Some((bytes.sha1_digest, chunk))) } } sealed case class Blob( name: Document.Node.Name, src_path: Path, content: Option[(SHA1.Digest, Symbol.Text_Chunk)]) { def read_file: Bytes = Bytes.read(name.path) def chunk_file: Symbol.Text_Chunk.File = Symbol.Text_Chunk.File(name.node) } object Blobs_Info { val none: Blobs_Info = Blobs_Info(Nil) def errors(msgs: List[String]): Blobs_Info = Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg)))) } sealed case class Blobs_Info(blobs: List[Exn.Result[Blob]], index: Int = -1) /** accumulated results from prover **/ /* results */ object Results { type Entry = (Long, XML.Elem) val empty: Results = new Results(SortedMap.empty) def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) } final class Results private(private val rep: SortedMap[Long, XML.Elem]) { def is_empty: Boolean = rep.isEmpty def defined(serial: Long): Boolean = rep.isDefinedAt(serial) def get(serial: Long): Option[XML.Elem] = rep.get(serial) def iterator: Iterator[Results.Entry] = rep.iterator def + (entry: Results.Entry): Results = if (defined(entry._1)) this else new Results(rep + entry) def ++ (other: Results): Results = if (this eq other) this else if (rep.isEmpty) other else (this /: other.iterator)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Results => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Results(", ", ", ")") } /* exports */ object Exports { type Entry = (Long, Export.Entry) val empty: Exports = new Exports(SortedMap.empty) def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _) } final class Exports private(private val rep: SortedMap[Long, Export.Entry]) { def is_empty: Boolean = rep.isEmpty def iterator: Iterator[Exports.Entry] = rep.iterator def + (entry: Exports.Entry): Exports = if (rep.isDefinedAt(entry._1)) this else new Exports(rep + entry) def ++ (other: Exports): Exports = if (this eq other) this else if (rep.isEmpty) other else (this /: other.iterator)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Exports => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Exports(", ", ", ")") } /* markups */ object Markup_Index { val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) def blob(blob: Blob): Markup_Index = Markup_Index(false, blob.chunk_file) } sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) object Markups { 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: TraversableOnce[Entry]): Markups = (empty /: args)(_ + _) def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _) } final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) { def is_empty: Boolean = rep.isEmpty def apply(index: Markup_Index): Markup_Tree = rep.getOrElse(index, Markup_Tree.empty) def add(index: Markup_Index, markup: Text.Markup): Markups = new Markups(rep + (index -> (this(index) + markup))) def + (entry: Markups.Entry): Markups = { val (index, tree) = entry new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full)))) } def ++ (other: Markups): Markups = if (this eq other) this else if (rep.isEmpty) other else (this /: other.rep.iterator)(_ + _) def redirection_iterator: Iterator[Document_ID.Generic] = for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) yield id def redirect(other_id: Document_ID.Generic): Markups = { val rep1 = (for { (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator if other_id == id } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap if (rep1.isEmpty) Markups.empty else new Markups(rep1) } override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Markups => rep == other.rep case _ => false } override def toString: String = rep.iterator.mkString("Markups(", ", ", ")") } /* state */ object State { def get_result(states: List[State], serial: Long): Option[XML.Elem] = states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get) def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] = for { serial <- Markup.Serial.unapply(props) elem <- get_result(states, serial) if elem.body.nonEmpty } yield serial -> elem def merge_results(states: List[State]): Results = Results.merge(states.map(_.results)) def merge_exports(states: List[State]): Exports = Exports.merge(states.map(_.exports)) def merge_markups(states: List[State]): Markups = Markups.merge(states.map(_.markups)) def merge_markup(states: List[State], index: Markup_Index, range: Text.Range, elements: Markup.Elements): Markup_Tree = Markup_Tree.merge(states.map(_.markup(index)), range, elements) def merge(command: Command, states: List[State]): State = State(command, states.flatMap(_.status), merge_results(states), merge_exports(states), merge_markups(states)) } sealed case class State( command: Command, status: List[Markup] = Nil, results: Results = Results.empty, exports: Exports = Exports.empty, markups: Markups = Markups.empty) { def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED) def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING) def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED) lazy val maybe_consolidated: Boolean = { var touched = false var forks = 0 var runs = 0 for (markup <- status) { markup.name match { case Markup.FORKED => touched = true; forks += 1 case Markup.JOINED => forks -= 1 case Markup.RUNNING => touched = true; runs += 1 case Markup.FINISHED => runs -= 1 case _ => } } touched && forks == 0 && runs == 0 } lazy val document_status: Document_Status.Command_Status = { val warnings = if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))) List(Markup(Markup.WARNING, Nil)) else Nil val errors = if (results.iterator.exists(p => Protocol.is_error(p._2))) List(Markup(Markup.ERROR, Nil)) else Nil Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator) } def markup(index: Markup_Index): Markup_Tree = markups(index) def redirect(other_command: Command): Option[State] = { val markups1 = markups.redirect(other_command.id) if (markups1.is_empty) None else Some(new State(other_command, markups = markups1)) } private def add_status(st: Markup): State = copy(status = st :: status) private def add_result(entry: Results.Entry): State = copy(results = results + entry) def add_export(entry: Exports.Entry): Option[State] = if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry)) else None private def add_markup( status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = { val markups1 = if (status || Document_Status.Command_Status.liberal_elements(m.info.name)) markups.add(Markup_Index(true, chunk_name), m) else markups copy(markups = markups1.add(Markup_Index(false, chunk_name), m)) } def accumulate( self_id: Document_ID.Generic => Boolean, other_id: (Document.Node.Name, Document_ID.Generic) => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], message: XML.Elem, cache: XML.Cache): State = message match { 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 }) } case XML.Elem(Markup(Markup.REPORT, atts0), msgs) => (this /: msgs)((state, msg) => { def bad(): Unit = Output.warning("Ignored report message: " + msg) msg match { case XML.Elem(Markup(name, atts), args) => command.reported_position(atts) orElse command.reported_position(atts0) match { case Some((id, chunk_name, target_range)) => val target = if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) Some((chunk_name, command.chunks(chunk_name))) else if (chunk_name == Symbol.Text_Chunk.Default) other_id(command.node_name, id) else None (target, target_range) match { case (Some((target_name, target_chunk)), Some(symbol_range)) if !symbol_range.is_singularity => target_chunk.incorporate(symbol_range) match { case Some(range) => val props = atts.filterNot(Markup.position_property) val elem = cache.elem(XML.Elem(Markup(name, props), args)) state.add_markup(false, target_name, Text.Info(range, elem)) case None => bad(); state } case _ => // silently ignore excessive reports state } case _ => bad(); state } case _ => bad(); state } }) case XML.Elem(Markup(name, props), body) => props match { case Markup.Serial(i) => val markup_message = cache.elem(XML.Elem(Markup(Markup.message(name), props), body)) val message_markup = cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))) var st = add_result(i -> markup_message) if (Protocol.is_inlined(message)) { for { (chunk_name, chunk) <- command.chunks.iterator range <- command.message_positions(self_id, chunk_name, chunk, message) } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup)) } st case _ => Output.warning("Ignored message without serial number: " + message) this } } } /** static content **/ /* make commands */ def apply( id: Document_ID.Command, node_name: Document.Node.Name, blobs_info: Blobs_Info, span: Command_Span.Span): Command = { val (source, span1) = span.compact_source new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty) } val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, Blobs_Info.none, Command_Span.empty) def unparsed( source: String, theory: Boolean = false, id: Document_ID.Command = Document_ID.none, node_name: Document.Node.Name = Document.Node.Name.empty, blobs_info: Blobs_Info = Blobs_Info.none, results: Results = Results.empty, markups: Markups = Markups.empty): Command = { val (source1, span1) = Command_Span.unparsed(source, theory).compact_source new Command(id, node_name, blobs_info, span1, source1, results, markups) } def text(source: String): Command = unparsed(source) def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = unparsed(XML.content(body), id = id, results = results, markups = Markups.init(Markup_Tree.from_XML(body))) /* edits and perspective */ type Edit = (Option[Command], Option[Command]) object Perspective { val empty: Perspective = Perspective(Nil) } sealed case class Perspective(commands: List[Command]) // visible commands in canonical order { def is_empty: Boolean = commands.isEmpty def same(that: Perspective): Boolean = { val cmds1 = this.commands val cmds2 = that.commands - require(!cmds1.exists(_.is_undefined)) - require(!cmds2.exists(_.is_undefined)) + require(!cmds1.exists(_.is_undefined), "cmds1 not defined") + require(!cmds2.exists(_.is_undefined), "cmds2 not defined") cmds1.length == cmds2.length && (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) } } /* blobs: inlined errors and auxiliary files */ def blobs_info( resources: Resources, syntax: Outer_Syntax, get_blob: Document.Node.Name => Option[Document.Blob], can_import: Document.Node.Name => Boolean, node_name: Document.Node.Name, span: Command_Span.Span): Blobs_Info = { span.name match { // inlined errors case Thy_Header.THEORY => val reader = span.content_reader val header = resources.check_thy(node_name, span.content_reader) val imports_pos = header.imports_pos val raw_imports = try { val read_imports = Thy_Header.read(node_name, reader).imports.map(_._1) if (imports_pos.length == read_imports.length) read_imports else error("") } catch { case _: Throwable => List.fill(header.imports.length)("") } val errors = for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) } yield { val completion = if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil "Bad theory import " + Markup.Path(import_name.node).markup(quote(import_name.toString)) + Position.here(pos) + Completion.report_theories(pos, completion) } Blobs_Info.errors(errors) // auxiliary files case _ => val loaded_files = span.loaded_files(syntax) val blobs = loaded_files.files.map(file => (Exn.capture { val src_path = Path.explode(file) val name = Document.Node.Name(resources.append(node_name, src_path)) val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk)) Blob(name, src_path, content) }).user_error) Blobs_Info(blobs, index = loaded_files.index) } } def build_blobs_info( syntax: Outer_Syntax, node_name: Document.Node.Name, load_commands: List[Command_Span.Span]): Blobs_Info = { val blobs = for { span <- load_commands file <- span.loaded_files(syntax).files } yield { (Exn.capture { val dir = node_name.master_dir_path val src_path = Path.explode(file) val name = Document.Node.Name((dir + src_path).expand.implode_symbolic) Blob.read_file(name, src_path) }).user_error } Blobs_Info(blobs) } } final class Command private( val id: Document_ID.Command, val node_name: Document.Node.Name, val blobs_info: Command.Blobs_Info, val span: Command_Span.Span, val source: String, val init_results: Command.Results, val init_markups: Command.Markups) { override def toString: String = id + "/" + span.kind.toString /* classification */ def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span] def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span def is_undefined: Boolean = id == Document_ID.none val is_unparsed: Boolean = span.content.exists(_.is_unparsed) val is_unfinished: Boolean = span.content.exists(_.is_unfinished) def potentially_initialized: Boolean = span.name == Thy_Header.THEORY /* blobs */ def blobs: List[Exn.Result[Command.Blob]] = blobs_info.blobs def blobs_index: Int = blobs_info.index def blobs_ok: Boolean = blobs.forall({ case Exn.Res(_) => true case _ => false }) def blobs_names: List[Document.Node.Name] = for (Exn.Res(blob) <- blobs) yield blob.name def blobs_undefined: List[Document.Node.Name] = for (Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] = for (Exn.Res(blob) <- blobs; (digest, _) <- blob.content) yield (blob.name, digest) def blobs_changed(doc_blobs: Document.Blobs): Boolean = blobs.exists({ case Exn.Res(blob) => doc_blobs.changed(blob.name) case _ => false }) /* source chunks */ val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = ((Symbol.Text_Chunk.Default -> chunk) :: (for (Exn.Res(blob) <- blobs; (_, file) <- blob.content) yield blob.chunk_file -> file)).toMap def length: Int = source.length def range: Text.Range = chunk.range val core_range: Text.Range = Text.Range(0, (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length)) def source(range: Text.Range): String = range.substring(source) /* theory parents */ def theory_parents(resources: Resources): List[Document.Node.Name] = if (span.name == Thy_Header.THEORY) { try { val header = Thy_Header.read(node_name, span.content_reader) for ((s, _) <- header.imports) yield { try { resources.import_name(node_name, s) } catch { case ERROR(_) => Document.Node.Name.empty } } } catch { case ERROR(_) => Nil } } else Nil /* reported positions */ def reported_position(pos: Position.T) : Option[(Document_ID.Generic, Symbol.Text_Chunk.Name, Option[Symbol.Range])] = { pos match { case Position.Id(id) => val chunk_name = pos match { case Position.File(name) if name != node_name.node => Symbol.Text_Chunk.File(name) case _ => Symbol.Text_Chunk.Default } Some((id, chunk_name, Position.Range.unapply(pos))) case _ => None } } def message_positions( self_id: Document_ID.Generic => Boolean, chunk_name: Symbol.Text_Chunk.Name, chunk: Symbol.Text_Chunk, message: XML.Elem): Set[Text.Range] = { def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = reported_position(props) match { case Some((id, name, reported_range)) if self_id(id) && name == chunk_name => val opt_range = reported_range orElse { if (name == Symbol.Text_Chunk.Default) Position.Range.unapply(span.position) else None } opt_range match { case Some(symbol_range) => chunk.incorporate(symbol_range) match { case Some(range) => set + range case _ => set } case None => set } case _ => set } def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] = t match { case XML.Wrapped_Elem(Markup(name, props), _, body) => body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) case XML.Elem(Markup(name, props), body) => body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) case XML.Text(_) => set } val set = tree(Set.empty, message) if (set.isEmpty) elem(message.markup.properties, set) else set } /* accumulated results */ val init_state: Command.State = Command.State(this, results = init_results, markups = init_markups) val empty_state: Command.State = Command.State(this) } diff --git a/src/Pure/PIDE/document.scala b/src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala +++ b/src/Pure/PIDE/document.scala @@ -1,1264 +1,1264 @@ /* Title: Pure/PIDE/document.scala Author: Makarius Document as collection of named nodes, each consisting of an editable list of commands, associated with asynchronous execution process. */ package isabelle import scala.collection.mutable object Document { /** document structure **/ /* overlays -- print functions with arguments */ object Overlays { val empty = new Overlays(Map.empty) } final class Overlays private(rep: Map[Node.Name, Node.Overlays]) { def apply(name: Node.Name): Node.Overlays = rep.getOrElse(name, Node.Overlays.empty) private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays = { val node_overlays = f(apply(name)) new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays)) } def insert(command: Command, fn: String, args: List[String]): Overlays = update(command.node_name, _.insert(command, fn, args)) def remove(command: Command, fn: String, args: List[String]): Overlays = update(command.node_name, _.remove(command, fn, args)) override def toString: String = rep.mkString("Overlays(", ",", ")") } /* document blobs: auxiliary files */ sealed case class Blob(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean) { def unchanged: Blob = copy(changed = false) } object Blobs { def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs) val empty: Blobs = apply(Map.empty) } final class Blobs private(blobs: Map[Node.Name, Blob]) { def get(name: Node.Name): Option[Blob] = blobs.get(name) def changed(name: Node.Name): Boolean = get(name) match { case Some(blob) => blob.changed case None => false } override def toString: String = blobs.mkString("Blobs(", ",", ")") } /* document nodes: theories and auxiliary files */ type Edit[A, B] = (Node.Name, Node.Edit[A, B]) type Edit_Text = Edit[Text.Edit, Text.Perspective] type Edit_Command = Edit[Command.Edit, Command.Perspective] object Node { /* header and name */ sealed case class Header( imports_pos: List[(Name, Position.T)] = Nil, keywords: Thy_Header.Keywords = Nil, abbrevs: Thy_Header.Abbrevs = Nil, errors: List[String] = Nil) { def imports_offset: Map[Int, Name] = (for { (name, Position.Offset(i)) <- imports_pos } yield i -> name).toMap def imports: List[Name] = imports_pos.map(_._1) def append_errors(msgs: List[String]): Header = copy(errors = errors ::: msgs) def cat_errors(msg2: String): Header = copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2))) } val no_header: Header = Header() def bad_header(msg: String): Header = Header(errors = List(msg)) object Name { val empty: Name = Name("") object Ordering extends scala.math.Ordering[Name] { def compare(name1: Name, name2: Name): Int = name1.node compare name2.node } type Graph[A] = isabelle.Graph[Node.Name, A] def make_graph[A](entries: List[((Name, A), List[Name])]): Graph[A] = Graph.make(entries, symmetric = true)(Ordering) } sealed case class Name(node: String, master_dir: String = "", theory: String = "") { override def hashCode: Int = node.hashCode override def equals(that: Any): Boolean = that match { case other: Name => node == other.node case _ => false } def path: Path = Path.explode(File.standard_path(node)) def master_dir_path: Path = Path.explode(File.standard_path(master_dir)) def expand: Name = Name(path.expand.implode, master_dir_path.expand.implode, theory) def symbolic: Name = Name(path.implode_symbolic, master_dir_path.implode_symbolic, theory) def is_theory: Boolean = theory.nonEmpty def theory_base_name: String = Long_Name.base_name(theory) override def toString: String = if (is_theory) theory else node def map(f: String => String): Name = copy(f(node), f(master_dir), theory) def map_theory(f: String => String): Name = copy(node, master_dir, f(theory)) def json: JSON.Object.T = JSON.Object("node_name" -> node, "theory_name" -> theory) } sealed case class Entry(name: Node.Name, header: Node.Header) { def map(f: String => String): Entry = copy(name = name.map(f)) override def toString: String = name.toString } /* node overlays */ object Overlays { val empty = new Overlays(Multi_Map.empty) } final class Overlays private(rep: Multi_Map[Command, (String, List[String])]) { def commands: Set[Command] = rep.keySet def is_empty: Boolean = rep.isEmpty def dest: List[(Command, (String, List[String]))] = rep.iterator.toList def insert(cmd: Command, fn: String, args: List[String]): Overlays = new Overlays(rep.insert(cmd, (fn, args))) def remove(cmd: Command, fn: String, args: List[String]): Overlays = new Overlays(rep.remove(cmd, (fn, args))) override def toString: String = rep.mkString("Node.Overlays(", ",", ")") } /* edits */ sealed abstract class Edit[A, B] { def foreach(f: A => Unit) { this match { case Edits(es) => es.foreach(f) case _ => } } def is_void: Boolean = this match { case Edits(Nil) => true case _ => false } } case class Blob[A, B](blob: Document.Blob) extends Edit[A, B] case class Edits[A, B](edits: List[A]) extends Edit[A, B] case class Deps[A, B](header: Header) extends Edit[A, B] case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B] /* perspective */ type Perspective_Text = Perspective[Text.Edit, Text.Perspective] type Perspective_Command = Perspective[Command.Edit, Command.Perspective] val no_perspective_text: Perspective_Text = Perspective(false, Text.Perspective.empty, Overlays.empty) val no_perspective_command: Perspective_Command = Perspective(false, Command.Perspective.empty, Overlays.empty) def is_no_perspective_text(perspective: Perspective_Text): Boolean = !perspective.required && perspective.visible.is_empty && perspective.overlays.is_empty def is_no_perspective_command(perspective: Perspective_Command): Boolean = !perspective.required && perspective.visible.is_empty && perspective.overlays.is_empty /* commands */ object Commands { def apply(commands: Linear_Set[Command]): Commands = new Commands(commands) val empty: Commands = apply(Linear_Set.empty) def starts(commands: Iterator[Command], offset: Text.Offset = 0) : Iterator[(Command, Text.Offset)] = { var i = offset for (command <- commands) yield { val start = i i += command.length (command, start) } } def starts_pos(commands: Iterator[Command], pos: Token.Pos = Token.Pos.start) : Iterator[(Command, Token.Pos)] = { var p = pos for (command <- commands) yield { val start = p p = (p /: command.span.content)(_.advance(_)) (command, start) } } private val block_size = 256 } final class Commands private(val commands: Linear_Set[Command]) { lazy val load_commands: List[Command] = commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = { val blocks = new mutable.ListBuffer[(Command, Text.Offset)] var next_block = 0 var last_stop = 0 for ((command, start) <- Commands.starts(commands.iterator)) { last_stop = start + command.length while (last_stop + 1 > next_block) { blocks += (command -> start) next_block += Commands.block_size } } (blocks.toArray, Text.Range(0, last_stop)) } private def full_range: Text.Range = full_index._2 def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = { if (commands.nonEmpty && full_range.contains(i)) { val (cmd0, start0) = full_index._1(i / Commands.block_size) Node.Commands.starts(commands.iterator(cmd0), start0) dropWhile { case (cmd, start) => start + cmd.length <= i } } else Iterator.empty } } val empty: Node = new Node() } final class Node private( val get_blob: Option[Document.Blob] = None, val header: Node.Header = Node.no_header, val syntax: Option[Outer_Syntax] = None, val text_perspective: Text.Perspective = Text.Perspective.empty, val perspective: Node.Perspective_Command = Node.no_perspective_command, _commands: Node.Commands = Node.Commands.empty) { def is_empty: Boolean = get_blob.isEmpty && header == Node.no_header && text_perspective.is_empty && Node.is_no_perspective_command(perspective) && commands.isEmpty def has_header: Boolean = header != Node.no_header override def toString: String = if (is_empty) "empty" else if (get_blob.isDefined) "blob" else "node" def commands: Linear_Set[Command] = _commands.commands def load_commands: List[Command] = _commands.load_commands def load_commands_changed(doc_blobs: Blobs): Boolean = load_commands.exists(_.blobs_changed(doc_blobs)) def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged)) def update_header(new_header: Node.Header): Node = new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands) def update_syntax(new_syntax: Option[Outer_Syntax]): Node = new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands) def update_perspective( new_text_perspective: Text.Perspective, new_perspective: Node.Perspective_Command): Node = new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands) def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] = Node.Perspective(perspective.required, text_perspective, perspective.overlays) def same_perspective( other_text_perspective: Text.Perspective, other_perspective: Node.Perspective_Command): Boolean = text_perspective == other_text_perspective && perspective.required == other_perspective.required && perspective.visible.same(other_perspective.visible) && perspective.overlays == other_perspective.overlays def update_commands(new_commands: Linear_Set[Command]): Node = if (new_commands eq _commands.commands) this else new Node(get_blob, header, syntax, text_perspective, perspective, Node.Commands(new_commands)) def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = _commands.iterator(i) def command_iterator(range: Text.Range): Iterator[(Command, Text.Offset)] = command_iterator(range.start) takeWhile { case (_, start) => start < range.stop } def command_start(cmd: Command): Option[Text.Offset] = Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2) def source: String = get_blob match { case Some(blob) => blob.source case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString } } /* development graph */ object Nodes { val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering)) } final class Nodes private(graph: Graph[Node.Name, Node]) { def apply(name: Node.Name): Node = graph.default_node(name, Node.empty).get_node(name) def is_suppressed(name: Node.Name): Boolean = { val graph1 = graph.default_node(name, Node.empty) graph1.is_maximal(name) && graph1.get_node(name).is_empty } 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(_)))) } def + (entry: (Node.Name, Node)): Nodes = { 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)) new Nodes(graph3.map_node(name, _ => node)) } def domain: Set[Node.Name] = graph.domain def iterator: Iterator[(Node.Name, Node)] = graph.iterator.map({ case (name, (node, _)) => (name, node) }) def theory_name(theory: String): Option[Node.Name] = graph.keys_iterator.find(name => name.theory == theory) def commands_loading(file_name: Node.Name): List[Command] = (for { (_, node) <- iterator cmd <- node.load_commands.iterator name <- cmd.blobs_names.iterator if name == file_name } yield cmd).toList def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names) def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds_rev(names) def topological_order: List[Node.Name] = graph.topological_order override def toString: String = topological_order.mkString("Nodes(", ",", ")") } /** versioning **/ /* particular document versions */ object Version { val init: Version = new Version() def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes) def purge_future(versions: Map[Document_ID.Version, Version], future: Future[Version]) : Future[Version] = { if (future.is_finished) { val version = future.join versions.get(version.id) match { case Some(version1) if !(version eq version1) => Future.value(version1) case _ => future } } else future } 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)))(_ + _) } } final class Version private( val id: Document_ID.Version = Document_ID.none, val nodes: Nodes = Nodes.empty) { override def toString: String = "Version(" + id + ")" def purge_suppressed: Option[Version] = nodes.purge_suppressed.map(new Version(id, _)) } /* changes of plain text, eventually resulting in document edits */ object Change { val init: Change = new Change() def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change = new Change(Some(previous), edits.reverse, version) } final class Change private( val previous: Option[Future[Version]] = Some(Future.value(Version.init)), val rev_edits: List[Edit_Text] = Nil, val version: Future[Version] = Future.value(Version.init)) { def is_finished: Boolean = (previous match { case None => true case Some(future) => future.is_finished }) && version.is_finished def truncate: Change = new Change(None, Nil, version) def purge(versions: Map[Document_ID.Version, Version]): Option[Change] = { val previous1 = previous.map(Version.purge_future(versions, _)) val version1 = Version.purge_future(versions, version) if ((previous eq previous1) && (version eq version1)) None else Some(new Change(previous1, rev_edits, version1)) } } /* history navigation */ object History { val init: History = new History() } final class History private( val undo_list: List[Change] = List(Change.init)) // non-empty list { override def toString: String = "History(" + undo_list.length + ")" def tip: Change = undo_list.head def + (change: Change): History = new History(change :: undo_list) def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] = { val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1 val (retained, dropped) = undo_list.splitAt(n max retain) retained.splitAt(retained.length - 1) match { case (prefix, List(last)) => Some(dropped, new History(prefix ::: List(last.truncate))) case _ => None } } def purge(versions: Map[Document_ID.Version, Version]): History = { val undo_list1 = undo_list.map(_.purge(versions)) if (undo_list1.forall(_.isEmpty)) this else new History(for ((a, b) <- undo_list1 zip undo_list) yield a.getOrElse(b)) } } /* snapshot: persistent user-view of document state */ object Snapshot { val init: Snapshot = State.init.snapshot() } class Snapshot private[Document]( val state: State, val version: Version, val node_name: Node.Name, edits: List[Text.Edit], val snippet_command: Option[Command]) { override def toString: String = "Snapshot(node = " + node_name.node + ", version = " + version.id + (if (is_outdated) ", outdated" else "") + ")" /* nodes */ def get_node(name: Node.Name): Node = version.nodes(name) val node: Node = get_node(node_name) def node_files: List[Node.Name] = node_name :: node.load_commands.flatMap(_.blobs_names) /* edits */ def is_outdated: Boolean = edits.nonEmpty private lazy val reverse_edits = edits.reverse def convert(offset: Text.Offset): Text.Offset = (offset /: edits)((i, edit) => edit.convert(i)) def revert(offset: Text.Offset): Text.Offset = (offset /: reverse_edits)((i, edit) => edit.revert(i)) def convert(range: Text.Range): Text.Range = range.map(convert) def revert(range: Text.Range): Text.Range = range.map(revert) /* theory load commands */ val commands_loading: List[Command] = if (node_name.is_theory) Nil else version.nodes.commands_loading(node_name) def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] = (for { cmd <- node.load_commands.iterator blob_name <- cmd.blobs_names.iterator if pred(blob_name) start <- node.command_start(cmd) } yield convert(cmd.core_range + start)).toList /* command as add-on snippet */ def snippet(command: Command): Snapshot = { val node_name = command.node_name val nodes0 = version.nodes val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) val version1 = Document.Version.make(nodes1) val edits: List[Edit_Text] = List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) val state0 = state.define_command(command) val state1 = state0.continue_history(Future.value(version), edits, Future.value(version1)) .define_version(version1, state0.the_assignment(version)) .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2 state1.snapshot(node_name = node_name, snippet_command = Some(command)) } /* XML markup */ def xml_markup( range: Text.Range = Text.Range.full, elements: Markup.Elements = Markup.Elements.full): XML.Body = state.xml_markup(version, node_name, range = range, elements = elements) def xml_markup_blobs(elements: Markup.Elements = Markup.Elements.full) : List[(Path, XML.Body)] = { snippet_command match { case None => Nil case Some(command) => for (Exn.Res(blob) <- command.blobs) yield { val bytes = blob.read_file val text = bytes.text val xml = if (Bytes(text) == bytes) { val markup = command.init_markups(Command.Markup_Index.blob(blob)) markup.to_XML(Text.Range(0, text.length), text, elements) } else Nil blob.src_path -> xml } } } /* messages */ lazy val messages: List[(XML.Elem, Position.T)] = (for { (command, start) <- Document.Node.Commands.starts_pos( node.commands.iterator, Token.Pos.file(node_name.node)) pos = command.span.keyword_pos(start).position(command.span.name) (_, elem) <- state.command_results(version, command).iterator } yield (elem, pos)).toList /* exports */ lazy val exports: List[Export.Entry] = state.node_exports(version, node_name).iterator.map(_._2).toList lazy val exports_map: Map[String, Export.Entry] = (for (entry <- exports.iterator) yield (entry.name, entry)).toMap /* find command */ def find_command(id: Document_ID.Generic): Option[(Node, Command)] = state.lookup_id(id) match { case None => None case Some(st) => val command = st.command val command_node = get_node(command.node_name) if (command_node.commands.contains(command)) Some((command_node, command)) else None } def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset) : Option[Line.Node_Position] = for ((node, command) <- find_command(id)) yield { val name = command.node_name.node val sources_iterator = 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(_)) Line.Node_Position(name, pos) } def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] = if (other_node_name.is_theory) { val other_node = get_node(other_node_name) val iterator = other_node.command_iterator(revert(offset) max 0) if (iterator.hasNext) { val (command0, _) = iterator.next other_node.commands.reverse.iterator(command0).find(command => !command.is_ignored) } else other_node.commands.reverse.iterator.find(command => !command.is_ignored) } else version.nodes.commands_loading(other_node_name).headOption /* command results */ def command_results(range: Text.Range): Command.Results = Command.State.merge_results( select[List[Command.State]](range, Markup.Elements.full, command_states => { case _ => Some(command_states) }).flatMap(_.info)) def command_results(command: Command): Command.Results = state.command_results(version, command) /* command ids: static and dynamic */ def command_id_map: Map[Document_ID.Generic, Command] = state.command_id_map(version, get_node(node_name).commands) /* cumulate markup */ def cumulate[A]( range: Text.Range, info: A, elements: Markup.Elements, result: List[Command.State] => (A, Text.Markup) => Option[A], status: Boolean = false): List[Text.Info[A]] = { val former_range = revert(range).inflate_singularity val (chunk_name, command_iterator) = commands_loading.headOption match { case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range)) case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0))) } val markup_index = Command.Markup_Index(status, chunk_name) (for { (command, command_start) <- command_iterator chunk <- command.chunks.get(chunk_name).iterator states = state.command_states(version, command) res = result(states) markup_range <- (former_range - command_start).try_restrict(chunk.range).iterator markup = Command.State.merge_markup(states, markup_index, markup_range, elements) Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements, { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }).iterator r1 <- convert(r0 + command_start).try_restrict(range).iterator } yield Text.Info(r1, a)).toList } def select[A]( range: Text.Range, elements: Markup.Elements, result: List[Command.State] => Text.Markup => Option[A], status: Boolean = false): List[Text.Info[A]] = { def result1(states: List[Command.State]): (Option[A], Text.Markup) => Option[Option[A]] = { val res = result(states) (_: Option[A], x: Text.Markup) => res(x) match { case None => None case some => Some(some) } } for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status)) yield Text.Info(r, x) } } /* model */ trait Session { def resources: Resources } trait Model { def session: Session def is_stable: Boolean def snapshot(): Snapshot def node_name: Node.Name def is_theory: Boolean = node_name.is_theory override def toString: String = node_name.toString def get_text(range: Text.Range): Option[String] def node_required: Boolean def get_blob: Option[Blob] def bibtex_entries: List[Text.Info[String]] def node_edits( node_header: Node.Header, text_edits: List[Text.Edit], perspective: Node.Perspective_Text): List[Edit_Text] = { val edits: List[Node.Edit[Text.Edit, Text.Perspective]] = get_blob match { case None => List( Node.Deps( if (session.resources.session_base.loaded_theory(node_name)) { node_header.append_errors( List("Cannot update finished theory " + quote(node_name.theory))) } else node_header), Node.Edits(text_edits), perspective) case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits)) } edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit)) } } /** global state -- document structure, execution process, editing history **/ type Assign_Update = List[(Document_ID.Command, List[Document_ID.Exec])] // update of exec state assignment object State { class Fail(state: State) extends Exception object Assignment { val init: Assignment = new Assignment() } final class Assignment private( val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty, val is_finished: Boolean = false) { override def toString: String = "Assignment(" + command_execs.size + "," + is_finished + ")" - def check_finished: Assignment = { require(is_finished); this } + def check_finished: Assignment = { require(is_finished, "assignment not finished"); this } def unfinished: Assignment = new Assignment(command_execs, false) def assign(update: Assign_Update): Assignment = { - require(!is_finished) + require(!is_finished, "assignment already finished") val command_execs1 = (command_execs /: update) { case (res, (command_id, exec_ids)) => if (exec_ids.isEmpty) res - command_id else res + (command_id -> exec_ids) } new Assignment(command_execs1, true) } } val init: State = State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2 } final case class State private( /*reachable versions*/ versions: Map[Document_ID.Version, Version] = Map.empty, /*inlined auxiliary files*/ blobs: Set[SHA1.Digest] = Set.empty, /*loaded theories in batch builds*/ theories: Map[Document_ID.Exec, Command.State] = Map.empty, /*static markup from define_command*/ commands: Map[Document_ID.Command, Command.State] = Map.empty, /*dynamic markup from execution*/ execs: Map[Document_ID.Exec, Command.State] = Map.empty, /*command-exec assignment for each version*/ assignments: Map[Document_ID.Version, State.Assignment] = Map.empty, /*commands with markup produced by other commands (imm_succs)*/ commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long, /*explicit (linear) history*/ history: History = History.init, /*intermediate state between remove_versions/removed_versions*/ removing_versions: Boolean = false) { override def toString: String = "State(versions = " + versions.size + ", blobs = " + blobs.size + ", commands = " + commands.size + ", execs = " + execs.size + ", assignments = " + assignments.size + ", commands_redirection = " + commands_redirection.size + ", history = " + history.undo_list.size + ", removing_versions = " + removing_versions + ")" private def fail[A]: A = throw new State.Fail(this) def define_version(version: Version, assignment: State.Assignment): State = { val id = version.id copy(versions = versions + (id -> version), assignments = assignments + (id -> assignment.unfinished)) } def define_blob(digest: SHA1.Digest): State = copy(blobs = blobs + digest) def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest) def define_command(command: Command): State = { val id = command.id if (commands.isDefinedAt(id)) fail else copy(commands = commands + (id -> command.init_state)) } def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id) def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail) def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail) def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail) def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail) def lookup_id(id: Document_ID.Generic): Option[Command.State] = theories.get(id) orElse commands.get(id) orElse execs.get(id) private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean = id == st.command.id || (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false }) private def other_id(node_name: Node.Name, id: Document_ID.Generic) : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = { for { st <- lookup_id(id) if st.command.node_name == node_name } yield (Symbol.Text_Chunk.Id(st.command.id), st.command.chunk) } 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) }) def accumulate(id: Document_ID.Generic, message: XML.Elem, cache: XML.Cache) : (Command.State, State) = { def update(st: Command.State): (Command.State, State) = { val st1 = st.accumulate(self_id(st), other_id, message, cache) (st1, copy(commands_redirection = redirection(st1))) } execs.get(id).map(update) match { case Some((st1, state1)) => (st1, state1.copy(execs = execs + (id -> st1))) case None => commands.get(id).map(update) match { case Some((st1, state1)) => (st1, state1.copy(commands = commands + (id -> st1))) case None => theories.get(id).map(update) match { case Some((st1, state1)) => (st1, state1.copy(theories = theories + (id -> st1))) case None => fail } } } } def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) = { execs.get(id) match { case Some(st) => st.add_export(entry) match { case Some(new_st) => (new_st, copy(execs = execs + (id -> new_st))) case None => fail } case None => commands.get(id) match { case Some(st) => st.add_export(entry) match { case Some(new_st) => (new_st, copy(commands = commands + (id -> new_st))) case None => fail } case None => fail } } } def node_exports(version: Version, node_name: Node.Name): Command.Exports = Command.Exports.merge( for { command <- version.nodes(node_name).commands.iterator st <- command_states(version, command).iterator } yield st.exports) def begin_theory( node_name: Node.Name, id: Document_ID.Exec, source: String, blobs_info: Command.Blobs_Info): State = { if (theories.isDefinedAt(id)) fail else { val command = Command.unparsed(source, theory = true, id = id, node_name = node_name, blobs_info = blobs_info) copy(theories = theories + (id -> command.empty_state)) } } def end_theory(id: Document_ID.Exec): (Snapshot, State) = theories.get(id) match { case None => fail case Some(st) => val command = st.command val node_name = command.node_name val command1 = Command.unparsed(command.source, theory = true, id = id, node_name = node_name, blobs_info = command.blobs_info, results = st.results, markups = st.markups) val state1 = copy(theories = theories - id) (state1.snippet(command1), state1) } def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) : ((List[Node.Name], List[Command]), State) = { val version = the_version(id) val edited_set = edited.toSet val edited_nodes = (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList def upd(exec_id: Document_ID.Exec, st: Command.State) : Option[(Document_ID.Exec, Command.State)] = if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st) val (changed_commands, new_execs) = ((Nil: List[Command], execs) /: update) { case ((commands1, execs1), (command_id, exec)) => val st = the_static_state(command_id) val command = st.command val commands2 = command :: commands1 val execs2 = exec match { case Nil => execs1 case eval_id :: print_ids => execs1 ++ upd(eval_id, st) ++ (for (id <- print_ids; up <- upd(id, command.empty_state)) yield up) } (commands2, execs2) } val new_assignment = the_assignment(version).assign(update) val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs) ((edited_nodes, changed_commands), new_state) } def is_assigned(version: Version): Boolean = assignments.get(version.id) match { case Some(assgn) => assgn.is_finished case None => false } def is_stable(change: Change): Boolean = change.is_finished && is_assigned(change.version.get_finished) def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail def stable_tip_version: Option[Version] = if (is_stable(history.tip)) Some(history.tip.version.get_finished) else None def continue_history( previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): State = { val change = Change.make(previous, edits, version) copy(history = history + change) } def remove_versions(retain: Int = 0): (List[Version], State) = { history.prune(is_stable, retain) match { case Some((dropped, history1)) => val old_versions = dropped.map(change => change.version.get_finished) val removing = old_versions.nonEmpty val state1 = copy(history = history1, removing_versions = removing) (old_versions, state1) case None => fail } } def removed_versions(removed: List[Document_ID.Version]): State = { val versions1 = Version.purge_suppressed(versions -- removed) val assignments1 = assignments -- removed var blobs1_names = Set.empty[Node.Name] var blobs1 = Set.empty[SHA1.Digest] var commands1 = Map.empty[Document_ID.Command, Command.State] var execs1 = Map.empty[Document_ID.Exec, Command.State] for { (version_id, version) <- versions1.iterator command_execs = assignments1(version_id).command_execs (_, node) <- version.nodes.iterator command <- node.commands.iterator } { for ((name, digest) <- command.blobs_defined) { blobs1_names += name blobs1 += digest } if (!commands1.isDefinedAt(command.id)) commands.get(command.id).foreach(st => commands1 += (command.id -> st)) for (exec_id <- command_execs.getOrElse(command.id, Nil)) { if (!execs1.isDefinedAt(exec_id)) execs.get(exec_id).foreach(st => execs1 += (exec_id -> st)) } } copy( versions = versions1, blobs = blobs1, commands = commands1, execs = execs1, commands_redirection = commands_redirection.restrict(commands1.keySet), assignments = assignments1, history = history.purge(versions1), removing_versions = false) } def command_id_map(version: Version, commands: Iterable[Command]) : Map[Document_ID.Generic, Command] = { - require(is_assigned(version)) + require(is_assigned(version), "version not assigned (command_id_map)") val assignment = the_assignment(version).check_finished (for { command <- commands.iterator id <- (command.id :: assignment.command_execs.getOrElse(command.id, Nil)).iterator } yield (id -> command)).toMap } def command_maybe_consolidated(version: Version, command: Command): Boolean = { - require(is_assigned(version)) + require(is_assigned(version), "version not assigned (command_maybe_consolidated)") try { the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match { case eval_id :: print_ids => the_dynamic_state(eval_id).maybe_consolidated && !print_ids.exists(print_id => the_dynamic_state(print_id).consolidating) case Nil => false } } catch { case _: State.Fail => false } } private def command_states_self(version: Version, command: Command) : List[(Document_ID.Generic, Command.State)] = { - require(is_assigned(version)) + require(is_assigned(version), "version not assigned (command_states_self)") try { the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) .map(id => id -> the_dynamic_state(id)) match { case Nil => fail case res => res } } catch { case _: State.Fail => try { List(command.id -> the_static_state(command.id)) } catch { case _: State.Fail => List(command.id -> command.init_state) } } } def command_states(version: Version, command: Command): List[Command.State] = { val self = command_states_self(version, command) val others = if (commands_redirection.defined(command.id)) { (for { command_id <- commands_redirection.imm_succs(command.id).iterator (id, st) <- command_states_self(version, the_static_state(command_id).command) if !self.exists(_._1 == id) } yield (id, st)).toMap.valuesIterator.toList } else Nil self.map(_._2) ::: others.flatMap(_.redirect(command)) } def command_results(version: Version, command: Command): Command.Results = Command.State.merge_results(command_states(version, command)) def command_markup(version: Version, command: Command, index: Command.Markup_Index, range: Text.Range, elements: Markup.Elements): Markup_Tree = Command.State.merge_markup(command_states(version, command), index, range, elements) def xml_markup( version: Version, node_name: Node.Name, range: Text.Range = Text.Range.full, elements: Markup.Elements = Markup.Elements.full): XML.Body = { val node = version.nodes(node_name) if (node_name.is_theory) { val markup_index = Command.Markup_Index.markup (for { command <- node.commands.iterator command_range <- command.range.try_restrict(range).iterator markup = command_markup(version, command, markup_index, command_range, elements) tree <- markup.to_XML(command_range, command.source, elements).iterator } yield tree).toList } else { val node_source = node.source Text.Range(0, node_source.length).try_restrict(range) match { case None => Nil case Some(node_range) => val markup = version.nodes.commands_loading(node_name).headOption match { case None => Markup_Tree.empty case Some(command) => val chunk_name = Symbol.Text_Chunk.File(node_name.node) val markup_index = Command.Markup_Index(false, chunk_name) command_markup(version, command, markup_index, node_range, elements) } markup.to_XML(node_range, node_source, elements) } } } def node_initialized(version: Version, name: Node.Name): Boolean = name.is_theory && (version.nodes(name).commands.iterator.find(_.potentially_initialized) match { case None => false case Some(command) => command_states(version, command).headOption.exists(_.initialized) }) def node_maybe_consolidated(version: Version, name: Node.Name): Boolean = name.is_theory && version.nodes(name).commands.reverse.iterator.forall(command_maybe_consolidated(version, _)) def node_consolidated(version: Version, name: Node.Name): Boolean = !name.is_theory || { val it = version.nodes(name).commands.reverse.iterator it.hasNext && command_states(version, it.next).exists(_.consolidated) } def snapshot( node_name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil, snippet_command: Option[Command] = None): Snapshot = { val stable = recent_stable val version = stable.version.get_finished val rev_pending_changes = for { change <- history.undo_list.takeWhile(_ != stable) (name, edits) <- change.rev_edits if name == node_name } yield edits val edits = (pending_edits /: rev_pending_changes)({ case (edits, Node.Edits(es)) => es ::: edits case (edits, _) => edits }) new Snapshot(this, version, node_name, edits, snippet_command) } def snippet(command: Command): Snapshot = snapshot().snippet(command) } } diff --git a/src/Pure/PIDE/headless.scala b/src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala +++ b/src/Pure/PIDE/headless.scala @@ -1,661 +1,661 @@ /* Title: Pure/PIDE/headless.scala Author: Makarius Headless PIDE session and resources from file-system. */ package isabelle import java.io.{File => JFile} import scala.annotation.tailrec import scala.collection.mutable object Headless { /** session **/ private def stable_snapshot( state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot = { val snapshot = state.snapshot(name) assert(version.id == snapshot.version.id) snapshot } class Use_Theories_Result private[Headless]( val state: Document.State, val version: Document.Version, val nodes: List[(Document.Node.Name, Document_Status.Node_Status)], val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)]) { def nodes_pending: List[(Document.Node.Name, Document_Status.Node_Status)] = { val committed = nodes_committed.iterator.map(_._1).toSet nodes.filter(p => !committed(p._1)) } def snapshot(name: Document.Node.Name): Document.Snapshot = stable_snapshot(state, version, name) def ok: Boolean = (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) } class Session private[Headless]( session_name: String, _session_options: => Options, override val resources: Resources) extends isabelle.Session(_session_options, resources) { session => private def loaded_theory(name: Document.Node.Name): Boolean = resources.session_base.loaded_theory(name.theory) /* options */ override def consolidate_delay: Time = session_options.seconds("headless_consolidate_delay") override def prune_delay: Time = session_options.seconds("headless_prune_delay") def default_check_delay: Time = session_options.seconds("headless_check_delay") def default_check_limit: Int = session_options.int("headless_check_limit") def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay") def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout") def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay") /* temporary directory */ val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session") val tmp_dir_name: String = File.path(tmp_dir).implode def master_directory(master_dir: String): String = proper_string(master_dir) getOrElse tmp_dir_name override def toString: String = session_name override def stop(): Process_Result = { try { super.stop() } finally { Isabelle_System.rm_tree(tmp_dir) } } /* theories */ private object Load_State { def finished: Load_State = Load_State(Nil, Nil, 0) def count_file(name: Document.Node.Name): Long = if (loaded_theory(name)) 0 else name.path.file.length } private case class Load_State( pending: List[Document.Node.Name], rest: List[Document.Node.Name], load_limit: Long) { def next( dep_graph: Document.Node.Name.Graph[Unit], finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Load_State) = { def load_requirements(pending1: List[Document.Node.Name], rest1: List[Document.Node.Name]) : (List[Document.Node.Name], Load_State) = { val load_theories = dep_graph.all_preds_rev(pending1).filterNot(finished) (load_theories, Load_State(pending1, rest1, load_limit)) } if (!pending.forall(finished)) (Nil, this) else if (rest.isEmpty) (Nil, Load_State.finished) else if (load_limit == 0) load_requirements(rest, Nil) else { val reachable = dep_graph.reachable_limit(load_limit, Load_State.count_file, dep_graph.imm_preds, rest) val (pending1, rest1) = rest.partition(reachable) load_requirements(pending1, rest1) } } } private sealed case class Use_Theories_State( dep_graph: Document.Node.Name.Graph[Unit], load_state: Load_State, watchdog_timeout: Time, commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit], last_update: Time = Time.now(), nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty, result: Option[Exn.Result[Use_Theories_Result]] = None) { def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = copy(last_update = Time.now(), nodes_status = new_nodes_status) def watchdog: Boolean = watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout def finished_result: Boolean = result.isDefined def join_result: Option[(Exn.Result[Use_Theories_Result], Use_Theories_State)] = if (finished_result) Some((result.get, this)) else None def cancel_result: Use_Theories_State = if (finished_result) this else copy(result = Some(Exn.Exn(Exn.Interrupt()))) def clean_theories: (List[Document.Node.Name], Use_Theories_State) = { @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name]) : Set[Document.Node.Name] = { val add = base.filter(name => dep_graph.imm_succs(name).forall(front)) if (add.isEmpty) front else { val preds = add.map(dep_graph.imm_preds) val base1 = (preds.head /: preds.tail)(_ ++ _).toList.filter(already_committed.keySet) frontier(base1, front ++ add) } } if (already_committed.isEmpty) (Nil, this) else { val base = (for { (name, (_, (_, succs))) <- dep_graph.iterator if succs.isEmpty && already_committed.isDefinedAt(name) } yield name).toList val clean = frontier(base, Set.empty) if (clean.isEmpty) (Nil, this) else { (dep_graph.topological_order.filter(clean), copy(dep_graph = dep_graph.exclude(clean))) } } } def check(state: Document.State, version: Document.Version, beyond_limit: Boolean) : (List[Document.Node.Name], Use_Theories_State) = { val already_committed1 = 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 }) } def finished_theory(name: Document.Node.Name): Boolean = loaded_theory(name) || (if (commit.isDefined) already_committed1.isDefinedAt(name) else state.node_consolidated(version, name)) val result1 = if (!finished_result && (beyond_limit || watchdog || dep_graph.keys_iterator.forall(name => finished_theory(name) || nodes_status.quasi_consolidated(name)))) { val nodes = (for { name <- dep_graph.keys_iterator if !loaded_theory(name) } yield { (name -> Document_Status.Node_Status.make(state, version, name)) }).toList val nodes_committed = (for { name <- dep_graph.keys_iterator status <- already_committed1.get(name) } yield (name -> status)).toList Some(Exn.Res(new Use_Theories_Result(state, version, nodes, nodes_committed))) } else result val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory) (load_theories, copy(already_committed = already_committed1, result = result1, load_state = load_state1)) } } def use_theories( theories: List[String], qualifier: String = Sessions.DRAFT, master_dir: String = "", unicode_symbols: Boolean = false, check_delay: Time = default_check_delay, check_limit: Int = default_check_limit, watchdog_timeout: Time = default_watchdog_timeout, nodes_status_delay: Time = default_nodes_status_delay, id: UUID.T = UUID.random(), // commit: must not block, must not fail commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None, commit_cleanup_delay: Time = default_commit_cleanup_delay, progress: Progress = new Progress): Use_Theories_Result = { val dependencies = { val import_names = theories.map(thy => resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none) resources.dependencies(import_names, progress = progress).check_errors } val dep_theories = dependencies.theories val dep_theories_set = dep_theories.toSet val dep_files = for (path <- dependencies.loaded_files) yield Document.Node.Name(resources.append("", path)) val use_theories_state = { val dep_graph = dependencies.theory_graph val maximals = dep_graph.maximals val rest = if (maximals.isEmpty || maximals.tail.isEmpty) maximals else { val depth = dep_graph.node_depth(Load_State.count_file) maximals.sortBy(node => - depth(node)) } val load_limit = if (commit.isDefined) (session_options.real("headless_load_limit") * 1024 * 1024).round else 0 val load_state = Load_State(Nil, rest, load_limit) Synchronized(Use_Theories_State(dep_graph, load_state, watchdog_timeout, commit)) } def check_state(beyond_limit: Boolean = false) { val state = session.get_state() for { version <- state.stable_tip_version load_theories = use_theories_state.change_result(_.check(state, version, beyond_limit)) if load_theories.nonEmpty } resources.load_theories(session, id, load_theories, dep_files, unicode_symbols, progress) } val check_progress = { var check_count = 0 Event_Timer.request(Time.now(), repeat = Some(check_delay)) { if (progress.stopped) use_theories_state.change(_.cancel_result) else { check_count += 1 check_state(check_limit > 0 && check_count > check_limit) } } } val consumer = { val delay_nodes_status = Delay.first(nodes_status_delay max Time.zero) { progress.nodes_status(use_theories_state.value.nodes_status) } val delay_commit_clean = Delay.first(commit_cleanup_delay max Time.zero) { val clean_theories = use_theories_state.change_result(_.clean_theories) if (clean_theories.nonEmpty) { progress.echo("Removing " + clean_theories.length + " theories ...") resources.clean_theories(session, id, clean_theories) } } Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => if (changed.nodes.exists(dep_theories_set)) { val snapshot = session.snapshot() val state = snapshot.state val version = snapshot.version val theory_progress = use_theories_state.change_result(st => { val domain = if (st.nodes_status.is_empty) dep_theories_set else changed.nodes.iterator.filter(dep_theories_set).toSet val (nodes_status_changed, nodes_status1) = st.nodes_status.update(resources, state, version, domain = Some(domain), trim = changed.assignment) if (nodes_status_delay >= Time.zero && nodes_status_changed) { delay_nodes_status.invoke } val theory_progress = (for { (name, node_status) <- nodes_status1.present.iterator if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name) p1 = node_status.percentage if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage) } yield Progress.Theory(name.theory, percentage = Some(p1))).toList (theory_progress, st.update(nodes_status1)) }) theory_progress.foreach(progress.theory) check_state() if (commit.isDefined && commit_cleanup_delay > Time.zero) { if (use_theories_state.value.finished_result) delay_commit_clean.revoke else delay_commit_clean.invoke } } } } try { session.commands_changed += consumer check_state() use_theories_state.guarded_access(_.join_result) check_progress.cancel } finally { session.commands_changed -= consumer resources.unload_theories(session, id, dep_theories) } Exn.release(use_theories_state.guarded_access(_.join_result)) } def purge_theories( theories: List[String], qualifier: String = Sessions.DRAFT, master_dir: String = "", all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) = { val nodes = if (all) None else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _))) resources.purge_theories(session, nodes) } } /** resources **/ object Resources { def apply(options: Options, base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources = new Resources(options, base_info, log = log) def make( options: Options, session_name: String, session_dirs: List[Path] = Nil, include_sessions: List[String] = Nil, progress: Progress = new Progress, log: Logger = No_Logger): Resources = { val base_info = Sessions.base_info(options, session_name, dirs = session_dirs, include_sessions = include_sessions, progress = progress) apply(options, base_info, log = log) } final class Theory private[Headless]( val node_name: Document.Node.Name, val node_header: Document.Node.Header, val text: String, val node_required: Boolean) { override def toString: String = node_name.toString def node_perspective: Document.Node.Perspective_Text = Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty) def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] = List(node_name -> Document.Node.Deps(node_header), node_name -> Document.Node.Edits(text_edits), node_name -> node_perspective) def node_edits(old: Option[Theory]): List[Document.Edit_Text] = { val (text_edits, old_required) = if (old.isEmpty) (Text.Edit.inserts(0, text), false) else (Text.Edit.replace(0, old.get.text, text), old.get.node_required) if (text_edits.isEmpty && node_required == old_required) Nil else make_edits(text_edits) } def purge_edits: List[Document.Edit_Text] = make_edits(Text.Edit.removes(0, text)) def required(required: Boolean): Theory = if (required == node_required) this else new Theory(node_name, node_header, text, required) } sealed case class State( blobs: Map[Document.Node.Name, Document.Blob] = Map.empty, theories: Map[Document.Node.Name, Theory] = Map.empty, required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty) { /* blobs */ def doc_blobs: Document.Blobs = Document.Blobs(blobs) def update_blobs(names: List[Document.Node.Name]): (Document.Blobs, State) = { val new_blobs = names.flatMap(name => { val bytes = Bytes.read(name.path) def new_blob: Document.Blob = { val text = bytes.text Document.Blob(bytes, text, Symbol.Text_Chunk(text), changed = true) } blobs.get(name) match { case Some(blob) => if (blob.bytes == bytes) None else Some(name -> new_blob) case None => Some(name -> new_blob) } }) val blobs1 = (blobs /: new_blobs)(_ + _) val blobs2 = (blobs /: new_blobs)({ case (map, (a, b)) => map + (a -> b.unchanged) }) (Document.Blobs(blobs1), copy(blobs = blobs2)) } def blob_edits(name: Document.Node.Name, old_blob: Option[Document.Blob]) : List[Document.Edit_Text] = { val blob = blobs.getOrElse(name, error("Missing blob " + quote(name.toString))) val text_edits = old_blob match { case None => List(Text.Edit.insert(0, blob.source)) case Some(blob0) => Text.Edit.replace(0, blob0.source, blob.source) } if (text_edits.isEmpty) Nil else List(name -> Document.Node.Blob(blob), name -> Document.Node.Edits(text_edits)) } /* theories */ lazy val theory_graph: Document.Node.Name.Graph[Unit] = Document.Node.Name.make_graph( for ((name, theory) <- theories.toList) yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt))) 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))) def remove_required(id: UUID.T, names: List[Document.Node.Name]): State = copy(required = (required /: names)(_.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) } })) def remove_theories(remove: List[Document.Node.Name]): State = { - require(remove.forall(name => !is_required(name))) + require(remove.forall(name => !is_required(name)), "attempt to remove required nodes") copy(theories = theories -- remove) } def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) : (List[Document.Edit_Text], State) = { val st1 = remove_required(id, theories) val theory_edits = for { node_name <- theories theory <- st1.theories.get(node_name) } yield { val theory1 = theory.required(st1.is_required(node_name)) val edits = theory1.node_edits(Some(theory)) (edits, (node_name, theory1)) } (theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2))) } def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) : ((List[Document.Node.Name], List[Document.Node.Name], List[Document.Edit_Text]), State) = { val all_nodes = theory_graph.topological_order val purge = nodes.getOrElse(all_nodes).filterNot(is_required).toSet val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet val (retained, purged) = all_nodes.partition(retain) val purge_edits = purged.flatMap(name => theories(name).purge_edits) ((purged, retained, purge_edits), remove_theories(purged)) } } } class Resources private[Headless]( val options: Options, val session_base_info: Sessions.Base_Info, log: Logger = No_Logger) extends isabelle.Resources( session_base_info.sessions_structure, session_base_info.check.base, log = log) { resources => val store: Sessions.Store = Sessions.store(options) /* session */ def start_session(print_mode: List[String] = Nil, progress: Progress = new Progress): Session = { val session = new Session(session_base_info.session, options, resources) 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 session } /* theories */ private val state = Synchronized(Resources.State()) def load_theories( session: Session, id: UUID.T, theories: List[Document.Node.Name], files: List[Document.Node.Name], unicode_symbols: Boolean, progress: Progress) { val loaded_theories = for (node_name <- theories) yield { val path = node_name.path if (!node_name.is_theory) error("Not a theory file: " + path) progress.expose_interrupt() val text0 = File.read(path) val text = if (unicode_symbols) Symbol.decode(text0) else text0 val node_header = resources.check_thy(node_name, Scan.char_reader(text)) new Resources.Theory(node_name, node_header, text, true) } val loaded = loaded_theories.length if (loaded > 1) progress.echo("Loading " + loaded + " theories ...") state.change(st => { val (doc_blobs1, st1) = st.insert_required(id, theories).update_blobs(files) val theory_edits = for (theory <- loaded_theories) yield { val node_name = theory.node_name val theory1 = theory.required(st1.is_required(node_name)) val edits = theory1.node_edits(st1.theories.get(node_name)) (edits, (node_name, theory1)) } val file_edits = for { node_name <- files if doc_blobs1.changed(node_name) } yield st1.blob_edits(node_name, st.blobs.get(node_name)) session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten) st1.update_theories(theory_edits.map(_._2)) }) } def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) { state.change(st => { val (edits, st1) = st.unload_theories(session, id, theories) session.update(st.doc_blobs, edits) st1 }) } def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) { state.change(st => { val (edits1, st1) = st.unload_theories(session, id, theories) val ((_, _, edits2), st2) = st1.purge_theories(session, None) session.update(st.doc_blobs, edits1 ::: edits2) st2 }) } def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) : (List[Document.Node.Name], List[Document.Node.Name]) = { state.change_result(st => { val ((purged, retained, _), st1) = st.purge_theories(session, nodes) ((purged, retained), st1) }) } } } diff --git a/src/Pure/PIDE/line.scala b/src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala +++ b/src/Pure/PIDE/line.scala @@ -1,253 +1,253 @@ /* Title: Pure/PIDE/line.scala Author: Makarius Line-oriented text documents, with some bias towards VSCode. */ package isabelle import scala.annotation.tailrec object Line { /* logical lines */ def normalize(text: String): String = if (text.contains('\r')) text.replace("\r\n", "\n") else text def logical_lines(text: String): List[String] = split_lines(normalize(text)) /* position */ object Position { val zero: Position = Position() val offside: Position = Position(line = -1) object Ordering extends scala.math.Ordering[Position] { def compare(p1: Position, p2: Position): Int = p1 compare p2 } } sealed case class Position(line: Int = 0, column: Int = 0) { def line1: Int = line + 1 def column1: Int = column + 1 def print: String = line1.toString + ":" + column1.toString def compare(that: Position): Int = line compare that.line match { case 0 => column compare that.column case i => i } def advance(text: String): Position = if (text.isEmpty) this else { val lines = logical_lines(text) val l = line + lines.length - 1 val c = (if (l == line) column else 0) + Library.trim_line(lines.last).length Position(l, c) } } /* range (right-open interval) */ object Range { def apply(start: Position): Range = Range(start, start) val zero: Range = Range(Position.zero) } sealed case class Range(start: Position, stop: Position) { if (start.compare(stop) > 0) error("Bad line range: " + start.print + ".." + stop.print) def print: String = if (start == stop) start.print else start.print + ".." + stop.print } /* positions within document node */ object Node_Position { def offside(name: String): Node_Position = Node_Position(name, Position.offside) } sealed case class Node_Position(name: String, pos: Position = Position.zero) { def line: Int = pos.line def line1: Int = pos.line1 def column: Int = pos.column def column1: Int = pos.column1 } sealed case class Node_Range(name: String, range: Range = Range.zero) { def start: Position = range.start def stop: Position = range.stop } /* document with newline as separator (not terminator) */ object Document { def apply(text: String): Document = Document(logical_lines(text).map(s => Line(Library.isolate_substring(s)))) val empty: Document = apply("") private def split(line_text: String): List[Line] = if (line_text == "") List(Line.empty) else apply(line_text).lines private def chop(lines: List[Line]): (String, List[Line]) = lines match { case Nil => ("", Nil) case line :: rest => (line.text, rest) } private def length(lines: List[Line]): Int = if (lines.isEmpty) 0 else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1 def text(lines: List[Line]): String = lines.mkString("", "\n", "") } sealed case class Document(lines: List[Line]) { lazy val text_length: Text.Offset = Document.length(lines) def text_range: Text.Range = Text.Range(0, text_length) lazy val text: String = Document.text(lines) def get_text(range: Text.Range): Option[String] = if (text_range.contains(range)) Some(range.substring(text)) else None override def toString: String = text override def equals(that: Any): Boolean = that match { case other: Document => lines == other.lines case _ => false } override def hashCode(): Int = lines.hashCode def position(text_offset: Text.Offset): Position = { @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position = { lines_rest match { - case Nil => require(i == 0); Position(lines_count) + case Nil => require(i == 0, "bad Line.position.move"); Position(lines_count) case line :: ls => val n = line.text.length if (ls.isEmpty || i <= n) Position(lines_count).advance(line.text.substring(n - i)) else move(i - (n + 1), lines_count + 1, ls) } } move(text_offset, 0, lines) } def range(text_range: Text.Range): Range = Range(position(text_range.start), position(text_range.stop)) def offset(pos: Position): Option[Text.Offset] = { val l = pos.line val c = pos.column val n = lines.length 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 } Some(line_offset + c) } else None } else if (l == n && c == 0) Some(text_length) else None } def change(remove: Range, insert: String): Option[(List[Text.Edit], Document)] = { for { edit_start <- offset(remove.start) if remove.stop == remove.start || offset(remove.stop).isDefined l1 = remove.start.line l2 = remove.stop.line if l1 <= l2 (removed_text, new_lines) <- { val c1 = remove.start.column val c2 = remove.stop.column val (prefix, lines1) = lines.splitAt(l1) val (s1, rest1) = Document.chop(lines1) if (l1 == l2) { if (0 <= c1 && c1 <= c2 && c2 <= s1.length) { Some( if (lines1.isEmpty) ("", prefix ::: Document.split(insert)) else { val removed_text = s1.substring(c1, c2) val changed_text = s1.substring(0, c1) + insert + s1.substring(c2) (removed_text, prefix ::: Document.split(changed_text) ::: rest1) }) } else None } else { val (middle, lines2) = rest1.splitAt(l2 - l1 - 1) val (s2, rest2) = Document.chop(lines2) if (0 <= c1 && c1 <= s1.length && 0 <= c2 && c2 <= s2.length) { Some( if (lines1.isEmpty) ("", prefix ::: Document.split(insert)) else { val r1 = s1.substring(c1) val r2 = s2.substring(0, c2) val removed_text = if (lines2.isEmpty) Document.text(Line(r1) :: middle) else Document.text(Line(r1) :: middle ::: List(Line(r2))) val changed_text = s1.substring(0, c1) + insert + s2.substring(c2) (removed_text, prefix ::: Document.split(changed_text) ::: rest2) }) } else None } } } yield (Text.Edit.removes(edit_start, removed_text) ::: Text.Edit.inserts(edit_start, insert), Document(new_lines)) } } /* line text */ val empty: Line = new Line("") def apply(text: String): Line = if (text == "") empty else new Line(text) } final class Line private(val text: String) { - require(text.forall(c => c != '\r' && c != '\n')) + require(text.forall(c => c != '\r' && c != '\n'), "bad line text") override def equals(that: Any): Boolean = that match { case other: Line => text == other.text case _ => false } override def hashCode(): Int = text.hashCode override def toString: String = text } diff --git a/src/Pure/PIDE/markup_tree.scala b/src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala +++ b/src/Pure/PIDE/markup_tree.scala @@ -1,268 +1,268 @@ /* Title: Pure/PIDE/markup_tree.scala Author: Fabian Immler, TU Munich Author: Makarius Markup trees over nested / non-overlapping text ranges. */ package isabelle import scala.collection.immutable.SortedMap import scala.collection.mutable import scala.annotation.tailrec object Markup_Tree { /* construct trees */ 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)) def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree = trees match { case Nil => empty case head :: tail => new Markup_Tree( (head.branches /: tail) { case (branches, tree) => (branches /: tree.branches) { case (bs, (r, entry)) => - require(!bs.isDefinedAt(r)) + require(!bs.isDefinedAt(r), "cannot merge markup trees") bs + (r -> entry) } }) } /* tree building blocks */ object Entry { def apply(markup: Text.Markup, subtree: Markup_Tree): Entry = Entry(markup.range, List(markup.info), subtree) } sealed case class Entry( range: Text.Range, rev_markup: List[XML.Elem], subtree: Markup_Tree) { def markup: List[XML.Elem] = rev_markup.reverse def filter_markup(elements: Markup.Elements): List[XML.Elem] = { var result: List[XML.Elem] = Nil for (elem <- rev_markup if elements(elem.name)) result ::= elem result } def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup) def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup) } object Branches { type T = SortedMap[Text.Range, Entry] val empty: T = SortedMap.empty(Text.Range.Ordering) } /* XML representation */ @tailrec private def strip_elems( elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) = body match { case List(XML.Wrapped_Elem(markup1, body1, body2)) => strip_elems(XML.Elem(markup1, body1) :: elems, body2) case List(XML.Elem(markup1, body1)) => strip_elems(XML.Elem(markup1, Nil) :: elems, body1) case _ => (elems, body) } private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) = { val (offset, markup_trees) = acc strip_elems(Nil, List(tree)) match { case (Nil, body) => (offset + XML.text_length(body), markup_trees) case (elems, body) => val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees) if (offset == end_offset) acc else { val range = Text.Range(offset, end_offset) val entry = Entry(range, elems, merge_disjoint(subtrees)) (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees) } } } def from_XML(body: XML.Body): Markup_Tree = merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2) } final class Markup_Tree private(val branches: Markup_Tree.Branches.T) { import Markup_Tree._ private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) = this(branches + (entry.range -> entry)) private def overlapping(range: Text.Range): Branches.T = if (branches.isEmpty || (range.contains(branches.firstKey.start) && branches.lastKey.stop <= range.stop)) branches else { val start = Text.Range(range.start) val stop = Text.Range(range.stop) val bs = branches.range(start, stop) branches.get(stop) match { case Some(end) if range overlaps end.range => bs + (end.range -> end) case _ => bs } } def restrict(range: Text.Range): Markup_Tree = new Markup_Tree(overlapping(range)) def is_empty: Boolean = branches.isEmpty def + (new_markup: Text.Markup): Markup_Tree = { val new_range = new_markup.range branches.get(new_range) match { case None => new Markup_Tree(branches, Entry(new_markup, empty)) case Some(entry) => if (entry.range == new_range) new Markup_Tree(branches, entry + new_markup) else if (entry.range.contains(new_range)) new Markup_Tree(branches, entry \ new_markup) else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1)) new Markup_Tree(Branches.empty, Entry(new_markup, this)) else { val body = overlapping(new_range) if (body.forall(e => new_range.contains(e._1))) new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body))) else { Output.warning("Ignored overlapping markup information: " + new_markup + "\n" + body.filter(e => !new_range.contains(e._1)).values.mkString("\n")) this } } } } 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) }) }) if (this eq other) this else { val tree1 = this.restrict(root_range) val tree2 = other.restrict(root_range) if (tree1.is_empty) tree2 else merge_trees(tree1, tree2) } } def cumulate[A](root_range: Text.Range, root_info: A, elements: Markup.Elements, result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] = { def results(x: A, entry: Entry): Option[A] = { var y = x var changed = false for { elem <- entry.filter_markup(elements) y1 <- result(y, Text.Info(entry.range, elem)) } { y = y1; changed = true } if (changed) Some(y) else None } def traverse( last: Text.Offset, stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] = { stack match { case (parent, (range, entry) :: more) :: rest => val subrange = range.restrict(root_range) val subtree = entry.subtree.overlapping(subrange).toList val start = subrange.start results(parent.info, entry) match { case Some(res) => val next = Text.Info(subrange, res) val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest) if (last < start) parent.restrict(Text.Range(last, start)) :: nexts else nexts case None => traverse(last, (parent, subtree ::: more) :: rest) } case (parent, Nil) :: rest => val stop = parent.range.stop val nexts = traverse(stop, rest) if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts else nexts case Nil => val stop = root_range.stop if (last < stop) List(Text.Info(Text.Range(last, stop), root_info)) else Nil } } traverse(root_range.start, List((Text.Info(root_range, root_info), overlapping(root_range).toList))) } def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body = { def make_text(start: Text.Offset, stop: Text.Offset): XML.Body = if (start == stop) Nil 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) { case (b, elem) => if (!elements(elem.name)) b else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b)) else List(XML.Wrapped_Elem(elem.markup, elem.body, b)) } def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T) : XML.Body = { val body = new mutable.ListBuffer[XML.Tree] var last = elem_range.start for ((range, entry) <- entries) { val subrange = range.restrict(elem_range) body ++= make_text(last, subrange.start) body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange)) last = subrange.stop } body ++= make_text(last, elem_range.stop) make_elems(elem_markup, body.toList) } make_body(root_range, Nil, overlapping(root_range)) } override def toString: String = branches.toList.map(_._2) match { case Nil => "Empty" case list => list.mkString("Tree(", ",", ")") } } diff --git a/src/Pure/PIDE/session.scala b/src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala +++ b/src/Pure/PIDE/session.scala @@ -1,776 +1,776 @@ /* Title: Pure/PIDE/session.scala Author: Makarius Options: :folding=explicit: PIDE editor session, potentially with running prover process. */ package isabelle import scala.collection.immutable.Queue import scala.collection.mutable import scala.annotation.tailrec object Session { /* outlets */ object Consumer { def apply[A](name: String)(consume: A => Unit): Consumer[A] = new Consumer[A](name, consume) } final class Consumer[-A] private(val name: String, val consume: A => Unit) class Outlet[A](dispatcher: Consumer_Thread[() => Unit]) { private val consumers = Synchronized[List[Consumer[A]]](Nil) def += (c: Consumer[A]) { consumers.change(Library.update(c)) } def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) } def post(a: A) { for (c <- consumers.value.iterator) { dispatcher.send(() => try { c.consume(a) } catch { case exn: Throwable => Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn)) }) } } } /* change */ sealed case class Change( previous: Document.Version, syntax_changed: List[Document.Node.Name], deps_changed: Boolean, doc_edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name], version: Document.Version) case object Change_Flush /* events */ //{{{ case class Command_Timing(props: Properties.T) case class Theory_Timing(props: Properties.T) case class Runtime_Statistics(props: Properties.T) case class Task_Statistics(props: Properties.T) case class Global_Options(options: Options) case object Caret_Focus case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])]) case class Commands_Changed( assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) sealed abstract class Phase { def print: String = this match { case Terminated(result) => if (result.ok) "finished" else "failed" case _ => Word.lowercase(this.toString) } } case object Inactive extends Phase // stable case object Startup extends Phase // transient case object Ready extends Phase // metastable case object Shutdown extends Phase // transient case class Terminated(result: Process_Result) extends Phase // stable //}}} /* syslog */ private[Session] class Syslog(limit: Int) { private var queue = Queue.empty[XML.Elem] private var length = 0 def += (msg: XML.Elem): Unit = synchronized { queue = queue.enqueue(msg) length += 1 if (length > limit) queue = queue.dequeue._2 } def content: String = synchronized { cat_lines(queue.iterator.map(XML.content)) + (if (length > limit) "\n(A total of " + length + " messages...)" else "") } } /* protocol handlers */ type Protocol_Function = Prover.Protocol_Output => Boolean abstract class Protocol_Handler extends Isabelle_System.Service { def init(session: Session): Unit = {} def exit(): Unit = {} def functions: List[(String, Protocol_Function)] = Nil def prover_options(options: Options): Options = options } } class Session(_session_options: => Options, val resources: Resources) extends Document.Session { session => val cache: XML.Cache = XML.Cache.make() def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none /* global flags */ @volatile var timing: Boolean = false @volatile var verbose: Boolean = false /* dynamic session options */ def session_options: Options = _session_options def output_delay: Time = session_options.seconds("editor_output_delay") def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay") def prune_delay: Time = session_options.seconds("editor_prune_delay") def prune_size: Int = session_options.int("editor_prune_size") def syslog_limit: Int = session_options.int("editor_syslog_limit") def reparse_limit: Int = session_options.int("editor_reparse_limit") /* dispatcher */ private val dispatcher = Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true } def assert_dispatcher[A](body: => A): A = { assert(dispatcher.check_thread) body } def require_dispatcher[A](body: => A): A = { - require(dispatcher.check_thread) + require(dispatcher.check_thread, "not on dispatcher thread") body } def send_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread) body else dispatcher.send(() => body) } def send_wait_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread) body else dispatcher.send_wait(() => body) } /* outlets */ val finished_theories = new Session.Outlet[Document.Snapshot](dispatcher) val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher) val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher) val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher) val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher) val global_options = new Session.Outlet[Session.Global_Options](dispatcher) val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher) val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher) val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher) val phase_changed = new Session.Outlet[Session.Phase](dispatcher) val syslog_messages = new Session.Outlet[Prover.Output](dispatcher) val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher) val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher) val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher) val all_messages = new Session.Outlet[Prover.Message](dispatcher) // potential bottle-neck! /** main protocol manager **/ /* internal messages */ private case class Start(start_prover: Prover.Receiver => Prover) private case object Stop private case class Get_State(promise: Promise[Document.State]) private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Protocol_Command(name: String, args: List[String]) private case class Update_Options(options: Options) private case object Consolidate_Execution private case object Prune_History /* phase */ private def post_phase(new_phase: Session.Phase): Session.Phase = { phase_changed.post(new_phase) new_phase } private val _phase = Synchronized[Session.Phase](Session.Inactive) private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase)) def phase: Session.Phase = _phase.value def is_ready: Boolean = phase == Session.Ready /* syslog */ private val syslog = new Session.Syslog(syslog_limit) def syslog_content(): String = syslog.content /* pipelined change parsing */ private case class Text_Edits( previous: Future[Document.Version], doc_blobs: Document.Blobs, text_edits: List[Document.Edit_Text], consolidate: List[Document.Node.Name], version_result: Promise[Document.Version]) private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) { case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) => val prev = previous.get_finished val change = Timing.timeit("parse_change", timing) { resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate) } version_result.fulfill(change.version) manager.send(change) true } /* buffered changes */ private object change_buffer { private var assignment: Boolean = false private var nodes: Set[Document.Node.Name] = Set.empty private var commands: Set[Command] = Set.empty def flush(): Unit = synchronized { if (assignment || nodes.nonEmpty || commands.nonEmpty) commands_changed.post(Session.Commands_Changed(assignment, nodes, commands)) if (nodes.nonEmpty) consolidation.update(nodes) assignment = false nodes = Set.empty commands = Set.empty } private val delay_flush = Delay.first(output_delay) { flush() } def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit = synchronized { assignment |= assign for (node <- edited_nodes) { nodes += node } for (command <- cmds) { nodes += command.node_name command.blobs_names.foreach(nodes += _) commands += command } delay_flush.invoke() } def shutdown() { delay_flush.revoke() flush() } } /* postponed changes */ private object postponed_changes { private var postponed: List[Session.Change] = Nil def store(change: Session.Change): Unit = synchronized { postponed ::= change } def flush(state: Document.State): List[Session.Change] = synchronized { val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous)) postponed = unassigned assigned.reverse } } /* node consolidation */ private object consolidation { private val delay = Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) } private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty) private val state = Synchronized(init_state) def exit() { delay.revoke() state.change(_ => None) } def update(new_nodes: Set[Document.Node.Name] = Set.empty) { val active = state.change_result(st => (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes))) if (active) delay.invoke() } def flush(): Set[Document.Node.Name] = state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None)) } /* prover process */ private object prover { private val variable = Synchronized[Option[Prover]](None) def defined: Boolean = variable.value.isDefined def get: Prover = variable.value.get def set(p: Prover) { variable.change(_ => Some(p)) } def reset { variable.change(_ => None) } def await_reset() { variable.guarded_access({ case None => Some((), None) case _ => None }) } } /* file formats and protocol handlers */ private lazy val file_formats: File_Format.Session = File_Format.registry.start_session(session) private val protocol_handlers = Protocol_Handlers.init(session) def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] = protocol_handlers.get(c.getName) match { case Some(h) if Library.is_subclass(h.getClass, c) => Some(h.asInstanceOf[C]) case _ => None } def init_protocol_handler(handler: Session.Protocol_Handler): Unit = protocol_handlers.init(handler) def prover_options(options: Options): Options = protocol_handlers.prover_options(file_formats.prover_options(options)) /* debugger */ private val debugger_handler = new Debugger.Handler(this) init_protocol_handler(debugger_handler) def debugger: Debugger = debugger_handler.debugger /* manager thread */ private val delay_prune = Delay.first(prune_delay) { manager.send(Prune_History) } private val manager: Consumer_Thread[Any] = { /* global state */ val global_state = Synchronized(Document.State.init) /* raw edits */ def handle_raw_edits( doc_blobs: Document.Blobs = Document.Blobs.empty, edits: List[Document.Edit_Text] = Nil, consolidate: List[Document.Node.Name] = Nil) //{{{ { - require(prover.defined) + require(prover.defined, "prover process not defined (handle_raw_edits)") if (edits.nonEmpty) prover.get.discontinue_execution() val previous = global_state.value.history.tip.version val version = Future.promise[Document.Version] global_state.change(_.continue_history(previous, edits, version)) raw_edits.post(Session.Raw_Edits(doc_blobs, edits)) change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version)) } //}}} /* resulting changes */ def handle_change(change: Session.Change) //{{{ { - require(prover.defined) + require(prover.defined, "prover process not defined (handle_change)") // define commands { val id_commands = new mutable.ListBuffer[Command] def id_command(command: Command) { for { (name, digest) <- command.blobs_defined if !global_state.value.defined_blob(digest) } { change.version.nodes(name).get_blob match { case Some(blob) => global_state.change(_.define_blob(digest)) prover.get.define_blob(digest, blob.bytes) case None => Output.error_message("Missing blob " + quote(name.toString)) } } if (!global_state.value.defined_command(command.id)) { global_state.change(_.define_command(command)) id_commands += command } } for { (_, edit) <- change.doc_edits } { edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) }) } if (id_commands.nonEmpty) { prover.get.define_commands_bulk(resources, id_commands.toList) } } val assignment = global_state.value.the_assignment(change.previous).check_finished global_state.change(_.define_version(change.version, assignment)) prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate) resources.commit(change) } //}}} /* prover output */ def handle_output(output: Prover.Output) //{{{ { def bad_output() { if (verbose) Output.warning("Ignoring bad prover output: " + output.message.toString) } def change_command(f: Document.State => (Command.State, Document.State)) { try { val st = global_state.change_result(f) if (!st.command.span.is_theory) { change_buffer.invoke(false, Nil, List(st.command)) } } catch { case _: Document.State.Fail => bad_output() } } output match { case msg: Prover.Protocol_Output => val handled = protocol_handlers.invoke(msg) if (!handled) { msg.properties match { case Protocol.Command_Timing(props, state_id, timing) if prover.defined => command_timings.post(Session.Command_Timing(props)) val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) change_command(_.accumulate(state_id, cache.elem(message), cache)) case Markup.Theory_Timing(props) => theory_timings.post(Session.Theory_Timing(props)) case Markup.Task_Statistics(props) => task_statistics.post(Session.Task_Statistics(props)) case Protocol.Export(args) if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => val id = Value.Long.unapply(args.id.get).get val export = Export.make_entry("", args, msg.bytes, cache) change_command(_.add_export(id, (args.serial, export))) case Protocol.Loading_Theory(node_name, id) => val blobs_info = build_blobs_info(node_name) try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) } catch { case _: Document.State.Fail => bad_output() } case List(Markup.Commands_Accepted.PROPERTY) => msg.text match { case Protocol.Commands_Accepted(ids) => ids.foreach(id => change_command(_.accumulate(id, Protocol.Commands_Accepted.message, cache))) case _ => bad_output() } case List(Markup.Assign_Update.PROPERTY) => msg.text match { case Protocol.Assign_Update(id, edited, update) => try { val (edited_nodes, cmds) = global_state.change_result(_.assign(id, edited, update)) change_buffer.invoke(true, edited_nodes, cmds) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } delay_prune.invoke() case List(Markup.Removed_Versions.PROPERTY) => msg.text match { case Protocol.Removed(removed) => try { global_state.change(_.removed_versions(removed)) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } case _ => bad_output() } } case _ => output.properties match { case Position.Id(state_id) => change_command(_.accumulate(state_id, output.message, cache)) case _ if output.is_init => val init_ok = try { Isabelle_System.make_services(classOf[Session.Protocol_Handler]) .foreach(init_protocol_handler) true } catch { case exn: Throwable => prover.get.protocol_command("Prover.stop", "1", Exn.message(exn)) false } if (init_ok) { prover.get.options(prover_options(session_options)) prover.get.init_session(resources) phase = Session.Ready debugger.ready() } case Markup.Process_Result(result) if output.is_exit => if (prover.defined) protocol_handlers.exit() for (id <- global_state.value.theories.keys) { val snapshot = global_state.change_result(_.end_theory(id)) finished_theories.post(snapshot) } file_formats.stop_session phase = Session.Terminated(result) prover.reset case _ => raw_output_messages.post(output) } } } //}}} /* main thread */ Consumer_Thread.fork[Any]("Session.manager", daemon = true) { case arg: Any => //{{{ arg match { case output: Prover.Output => if (output.is_syslog) { syslog += output.message syslog_messages.post(output) } if (output.is_stdout || output.is_stderr) raw_output_messages.post(output) else handle_output(output) all_messages.post(output) case input: Prover.Input => all_messages.post(input) case Start(start_prover) if !prover.defined => prover.set(start_prover(manager.send(_))) case Stop => consolidation.exit() delay_prune.revoke() if (prover.defined) { global_state.change(_ => Document.State.init) prover.get.terminate } case Get_State(promise) => promise.fulfill(global_state.value) case Consolidate_Execution => if (prover.defined) { val state = global_state.value state.stable_tip_version match { case None => consolidation.update() case Some(version) => val consolidate = consolidation.flush().iterator.filter(name => !resources.session_base.loaded_theory(name) && !state.node_consolidated(version, name) && state.node_maybe_consolidated(version, name)).toList if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate) } } case Prune_History => if (prover.defined) { val old_versions = global_state.change_result(_.remove_versions(prune_size)) if (old_versions.nonEmpty) prover.get.remove_versions(old_versions) } case Update_Options(options) => if (prover.defined && is_ready) { prover.get.options(prover_options(options)) handle_raw_edits() } global_options.post(Session.Global_Options(options)) case Cancel_Exec(exec_id) if prover.defined => prover.get.cancel_exec(exec_id) case Session.Raw_Edits(doc_blobs, edits) if prover.defined => handle_raw_edits(doc_blobs = doc_blobs, edits = edits) case Session.Dialog_Result(id, serial, result) if prover.defined => prover.get.dialog_result(serial, result) handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) case Protocol_Command(name, args) if prover.defined => prover.get.protocol_command_args(name, args) case change: Session.Change if prover.defined => val state = global_state.value if (!state.removing_versions && state.is_assigned(change.previous)) handle_change(change) else postponed_changes.store(change) case Session.Change_Flush if prover.defined => val state = global_state.value if (!state.removing_versions) postponed_changes.flush(state).foreach(handle_change) case bad => if (verbose) Output.warning("Ignoring bad message: " + bad.toString) } true //}}} } } /* main operations */ def get_state(): Document.State = { if (manager.is_active) { val promise = Future.promise[Document.State] manager.send_wait(Get_State(promise)) promise.join } else Document.State.init } def snapshot(name: Document.Node.Name = Document.Node.Name.empty, pending_edits: List[Text.Edit] = Nil): Document.Snapshot = get_state().snapshot(name, pending_edits) def recent_syntax(name: Document.Node.Name): Outer_Syntax = get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse resources.session_base.overall_syntax @tailrec final def await_stable_snapshot(): Document.Snapshot = { val snapshot = this.snapshot() if (snapshot.is_outdated) { output_delay.sleep await_stable_snapshot() } else snapshot } def start(start_prover: Prover.Receiver => Prover) { file_formats _phase.change( { case Session.Inactive => manager.send(Start(start_prover)) post_phase(Session.Startup) case phase => error("Cannot start prover in phase " + quote(phase.print)) }) } def stop(): Process_Result = { val was_ready = _phase.guarded_access( { case Session.Startup | Session.Shutdown => None case Session.Terminated(_) => Some((false, phase)) case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0))))) case Session.Ready => Some((true, post_phase(Session.Shutdown))) }) if (was_ready) manager.send(Stop) prover.await_reset() change_parser.shutdown() change_buffer.shutdown() manager.shutdown() dispatcher.shutdown() phase match { case Session.Terminated(result) => result case phase => error("Bad session phase after shutdown: " + quote(phase.print)) } } def protocol_command(name: String, args: String*) { manager.send(Protocol_Command(name, args.toList)) } def cancel_exec(exec_id: Document_ID.Exec) { manager.send(Cancel_Exec(exec_id)) } def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) { if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) } def update_options(options: Options) { manager.send_wait(Update_Options(options)) } def dialog_result(id: Document_ID.Generic, serial: Long, result: String) { manager.send(Session.Dialog_Result(id, serial, result)) } } diff --git a/src/Pure/System/cygwin.scala b/src/Pure/System/cygwin.scala --- a/src/Pure/System/cygwin.scala +++ b/src/Pure/System/cygwin.scala @@ -1,68 +1,68 @@ /* Title: Pure/System/cygwin.scala Author: Makarius Cygwin as POSIX emulation on Windows. */ package isabelle import java.io.{File => JFile} import java.nio.file.Files import scala.annotation.tailrec object Cygwin { /* init (e.g. after extraction via 7zip) */ def init(isabelle_root: String, cygwin_root: String) { - require(Platform.is_windows) + require(Platform.is_windows, "Windows platform expected") def exec(cmdline: String*) { val cwd = new JFile(isabelle_root) val env = sys.env + ("CYGWIN" -> "nodosfilewarning") val proc = Isabelle_System.process(cmdline.toList, cwd = cwd, env = env, redirect = true) val (output, rc) = Isabelle_System.process_output(proc) if (rc != 0) error(output) } val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") val uninitialized = uninitialized_file.isFile && uninitialized_file.delete if (uninitialized) { val symlinks = { val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]] } @tailrec def recover_symlinks(list: List[String]): Unit = { list match { case Nil | List("") => case target :: content :: rest => link(content, new JFile(isabelle_root, target)) recover_symlinks(rest) case _ => error("Unbalanced symlinks list") } } recover_symlinks(symlinks) exec(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall") exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall") } } def link(content: String, target: JFile) { val target_path = target.toPath using(Files.newBufferedWriter(target_path, UTF8.charset))( _.write("!" + content + "\u0000")) Files.setAttribute(target_path, "dos:system", true) } } diff --git a/src/Pure/System/linux.scala b/src/Pure/System/linux.scala --- a/src/Pure/System/linux.scala +++ b/src/Pure/System/linux.scala @@ -1,159 +1,159 @@ /* Title: Pure/System/linux.scala Author: Makarius Specific support for Linux, notably Ubuntu/Debian. */ package isabelle import scala.util.matching.Regex object Linux { /* check system */ def check_system(): Unit = if (!Platform.is_linux) error("Not a Linux system") def check_system_root(): Unit = { check_system() if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)") } /* release */ object Release { private val ID = """^Distributor ID:\s*(\S.*)$""".r private val RELEASE = """^Release:\s*(\S.*)$""".r private val DESCRIPTION = """^Description:\s*(\S.*)$""".r def apply(): Release = { val lines = Isabelle_System.bash("lsb_release -a").check.out_lines def find(R: Regex): String = lines.collectFirst({ case R(a) => a }).getOrElse("Unknown") new Release(find(ID), find(RELEASE), find(DESCRIPTION)) } } final class Release private(val id: String, val release: String, val description: String) { override def toString: String = description def is_ubuntu: Boolean = id == "Ubuntu" def is_ubuntu_18_04: Boolean = is_ubuntu && release == "18.04" def is_ubuntu_20_04: Boolean = is_ubuntu && release == "20.04" } /* packages */ def reboot_required(): Boolean = Path.explode("/var/run/reboot-required").is_file def check_reboot_required(): Unit = if (reboot_required()) error("Reboot required") def package_update(progress: Progress = new Progress): Unit = progress.bash( """apt-get update -y && apt-get upgrade -y && apt autoremove -y""", echo = true).check def package_install(packages: List[String], progress: Progress = new Progress): Unit = progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check def package_installed(name: String): Boolean = { val result = Isabelle_System.bash("dpkg-query -s " + Bash.string(name)) val pattern = """^Status:.*installed.*$""".r.pattern result.ok && result.out_lines.exists(line => pattern.matcher(line).matches) } /* users */ def user_exists(name: String): Boolean = Isabelle_System.bash("id " + Bash.string(name)).ok def user_entry(name: String, field: Int): String = { val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check val fields = space_explode(':', result.out) if (1 <= field && field <= fields.length) fields(field - 1) else error("No passwd field " + field + " for user " + quote(name)) } def user_description(name: String): String = user_entry(name, 5).takeWhile(_ != ',') def user_home(name: String): String = user_entry(name, 6) def user_add(name: String, description: String = "", system: Boolean = false, ssh_setup: Boolean = false) { - require(!description.contains(',')) + require(!description.contains(','), "malformed description") if (user_exists(name)) error("User already exists: " + quote(name)) Isabelle_System.bash( "adduser --quiet --disabled-password --gecos " + Bash.string(description) + (if (system) " --system --group --shell /bin/bash " else "") + " " + Bash.string(name)).check if (ssh_setup) { val id_rsa = user_home(name) + "/.ssh/id_rsa" Isabelle_System.bash(""" if [ ! -f """ + Bash.string(id_rsa) + """ ] then yes '\n' | sudo -i -u """ + Bash.string(name) + """ ssh-keygen -q -f """ + Bash.string(id_rsa) + """ fi """).check } } /* system services */ def service_operation(op: String, name: String): Unit = Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check def service_enable(name: String) { service_operation("enable", name) } def service_disable(name: String) { service_operation("disable", name) } def service_start(name: String) { service_operation("start", name) } def service_stop(name: String) { service_operation("stop", name) } def service_restart(name: String) { service_operation("restart", name) } def service_shutdown(name: String) { try { service_stop(name) } catch { case ERROR(_) => } } def service_install(name: String, spec: String) { service_shutdown(name) val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service") File.write(service_file, spec) Isabelle_System.chmod("644", service_file) service_enable(name) service_restart(name) } /* passwords */ def generate_password(length: Int = 10): String = { - require(length >= 6) + require(length >= 6, "password too short") Isabelle_System.bash("pwgen " + length + " 1").check.out } } diff --git a/src/Pure/Thy/bibtex.scala b/src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala +++ b/src/Pure/Thy/bibtex.scala @@ -1,701 +1,702 @@ /* Title: Pure/Thy/bibtex.scala Author: Makarius BibTeX support. */ package isabelle import java.io.{File => JFile} import scala.collection.mutable import scala.util.parsing.combinator.RegexParsers import scala.util.parsing.input.Reader object Bibtex { /** file format **/ def is_bibtex(name: String): Boolean = name.endsWith(".bib") class File_Format extends isabelle.File_Format { val format_name: String = "bibtex" val file_ext: String = "bib" override def theory_suffix: String = "bibtex_file" override def theory_content(name: String): String = """theory "bib" imports Pure begin bibtex_file """ + Outer_Syntax.quote_string(name) + """ end""" override def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = { val name = snapshot.node_name if (detect(name.node)) { val title = "Bibliography " + quote(snapshot.node_name.path.file_name) val content = Isabelle_System.with_tmp_file("bib", "bib") { bib => File.write(bib, snapshot.node.source) Bibtex.html_output(List(bib), style = "unsort", title = title) } Some(Presentation.HTML_Document(title, content)) } else None } } /** bibtex errors **/ def bibtex_errors(dir: Path, root_name: String): List[String] = { val log_path = dir + Path.explode(root_name).ext("blg") if (log_path.is_file) { val Error1 = """^(I couldn't open database file .+)$""".r val Error2 = """^(.+)---line (\d+) of file (.+)""".r Line.logical_lines(File.read(log_path)).flatMap(line => line match { case Error1(msg) => Some("Bibtex error: " + msg) case Error2(msg, Value.Int(l), file) => val path = File.standard_path(file) if (Path.is_wellformed(path)) { val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode) Some("Bibtex error" + Position.here(pos) + ":\n " + msg) } else None case _ => None }) } else Nil } /** check database **/ def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) = { val chunks = parse(Line.normalize(database)) var chunk_pos = Map.empty[String, Position.T] val tokens = new mutable.ListBuffer[(Token, Position.T)] var line = 1 var offset = 1 def make_pos(length: Int): Position.T = Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line) def advance_pos(tok: Token) { for (s <- Symbol.iterator(tok.source)) { if (Symbol.is_newline(s)) line += 1 offset += 1 } } def get_line_pos(l: Int): Position.T = if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none for (chunk <- chunks) { val name = chunk.name if (name != "" && !chunk_pos.isDefinedAt(name)) { chunk_pos += (name -> make_pos(chunk.heading_length)) } for (tok <- chunk.tokens) { tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length)) advance_pos(tok) } } Isabelle_System.with_tmp_dir("bibtex")(tmp_dir => { File.write(tmp_dir + Path.explode("root.bib"), tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n")) File.write(tmp_dir + Path.explode("root.aux"), "\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}") Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file) val Error = """^(.*)---line (\d+) of file root.bib$""".r val Warning = """^Warning--(.+)$""".r val Warning_Line = """--line (\d+) of file root.bib$""".r val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r val log_file = tmp_dir + Path.explode("root.blg") val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil val (errors, warnings) = if (lines.isEmpty) (Nil, Nil) else { lines.zip(lines.tail ::: List("")).flatMap( { case (Error(msg, Value.Int(l)), _) => Some((true, (msg, get_line_pos(l)))) case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) => Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name)))) case (Warning(msg), Warning_Line(Value.Int(l))) => Some((false, (Word.capitalize(msg), get_line_pos(l)))) case (Warning(msg), _) => Some((false, (Word.capitalize(msg), Position.none))) case _ => None } ).partition(_._1) } (errors.map(_._2), warnings.map(_._2)) }) } object Check_Database extends Scala.Fun("bibtex_check_database") { val here = Scala_Project.here def apply(database: String): String = { import XML.Encode._ YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))( check_database(database))) } } /** document model **/ /* entries */ def entries(text: String): List[Text.Info[String]] = { val result = new mutable.ListBuffer[Text.Info[String]] var offset = 0 for (chunk <- Bibtex.parse(text)) { val end_offset = offset + chunk.source.length if (chunk.name != "" && !chunk.is_command) result += Text.Info(Text.Range(offset, end_offset), chunk.name) offset = end_offset } result.toList } def entries_iterator[A, B <: Document.Model](models: Map[A, B]) : Iterator[Text.Info[(String, B)]] = { for { (_, model) <- models.iterator info <- model.bibtex_entries.iterator } yield info.map((_, model)) } /* completion */ def completion[A, B <: Document.Model]( history: Completion.History, rendering: Rendering, caret: Text.Offset, models: Map[A, B]): Option[Completion.Result] = { for { Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption name1 <- Completion.clean_name(name) original <- rendering.get_text(r) original1 <- Completion.clean_name(Library.perhaps_unquote(original)) entries = (for { Text.Info(_, (entry, _)) <- entries_iterator(models) if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1 } yield entry).toList if entries.nonEmpty items = entries.sorted.map({ case entry => val full_name = Long_Name.qualify(Markup.CITATION, entry) val description = List(entry, "(BibTeX entry)") val replacement = quote(entry) Completion.Item(r, original, full_name, description, replacement, 0, false) }).sorted(history.ordering).take(rendering.options.int("completion_limit")) } yield Completion.Result(r, original, false, items) } /** content **/ private val months = List( "jan", "feb", "mar", "apr", "may", "jun", "jul", "aug", "sep", "oct", "nov", "dec") def is_month(s: String): Boolean = months.contains(s.toLowerCase) private val commands = List("preamble", "string") def is_command(s: String): Boolean = commands.contains(s.toLowerCase) sealed case class Entry( kind: String, required: List[String], optional_crossref: List[String], optional_other: List[String]) { val optional_standard: List[String] = List("url", "doi", "ee") def is_required(s: String): Boolean = required.contains(s.toLowerCase) def is_optional(s: String): Boolean = optional_crossref.contains(s.toLowerCase) || optional_other.contains(s.toLowerCase) || optional_standard.contains(s.toLowerCase) def fields: List[String] = required ::: optional_crossref ::: optional_other ::: optional_standard def template: String = "@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n" } val known_entries: List[Entry] = List( Entry("Article", List("author", "title"), List("journal", "year"), List("volume", "number", "pages", "month", "note")), Entry("InProceedings", List("author", "title"), List("booktitle", "year"), List("editor", "volume", "number", "series", "pages", "month", "address", "organization", "publisher", "note")), Entry("InCollection", List("author", "title", "booktitle"), List("publisher", "year"), List("editor", "volume", "number", "series", "type", "chapter", "pages", "edition", "month", "address", "note")), Entry("InBook", List("author", "editor", "title", "chapter"), List("publisher", "year"), List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")), Entry("Proceedings", List("title", "year"), List(), List("booktitle", "editor", "volume", "number", "series", "address", "month", "organization", "publisher", "note")), Entry("Book", List("author", "editor", "title"), List("publisher", "year"), List("volume", "number", "series", "address", "edition", "month", "note")), Entry("Booklet", List("title"), List(), List("author", "howpublished", "address", "month", "year", "note")), Entry("PhdThesis", List("author", "title", "school", "year"), List(), List("type", "address", "month", "note")), Entry("MastersThesis", List("author", "title", "school", "year"), List(), List("type", "address", "month", "note")), Entry("TechReport", List("author", "title", "institution", "year"), List(), List("type", "number", "address", "month", "note")), Entry("Manual", List("title"), List(), List("author", "organization", "address", "edition", "month", "year", "note")), Entry("Unpublished", List("author", "title", "note"), List(), List("month", "year")), Entry("Misc", List(), List(), List("author", "title", "howpublished", "month", "year", "note"))) def get_entry(kind: String): Option[Entry] = known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase) def is_entry(kind: String): Boolean = get_entry(kind).isDefined /** tokens and chunks **/ object Token { object Kind extends Enumeration { val COMMAND = Value("command") val ENTRY = Value("entry") val KEYWORD = Value("keyword") val NAT = Value("natural number") val STRING = Value("string") val NAME = Value("name") val IDENT = Value("identifier") val SPACE = Value("white space") val COMMENT = Value("ignored text") val ERROR = Value("bad input") } } sealed case class Token(kind: Token.Kind.Value, source: String) { def is_kind: Boolean = kind == Token.Kind.COMMAND || kind == Token.Kind.ENTRY || kind == Token.Kind.IDENT def is_name: Boolean = kind == Token.Kind.NAME || kind == Token.Kind.IDENT def is_ignored: Boolean = kind == Token.Kind.SPACE || kind == Token.Kind.COMMENT def is_malformed: Boolean = kind == Token.Kind.ERROR def is_open: Boolean = kind == Token.Kind.KEYWORD && (source == "{" || source == "(") } case class Chunk(kind: String, tokens: List[Token]) { val source = tokens.map(_.source).mkString private val content: Option[List[Token]] = tokens match { case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty => (body.init.filterNot(_.is_ignored), body.last) match { case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}")) if tok.is_kind => Some(toks) case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")")) if tok.is_kind => Some(toks) case _ => None } case _ => None } def name: String = content match { case Some(tok :: _) if tok.is_name => tok.source case _ => "" } def heading_length: Int = if (name == "") 1 else (0 /: tokens.takeWhile(tok => !tok.is_open)){ 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) def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined } /** parsing **/ // context of partial line-oriented scans abstract class Line_Context case object Ignored extends Line_Context case object At extends Line_Context case class Item_Start(kind: String) extends Line_Context case class Item_Open(kind: String, end: String) extends Line_Context case class Item(kind: String, end: String, delim: Delimited) extends Line_Context case class Delimited(quoted: Boolean, depth: Int) val Closed = Delimited(false, 0) private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source) private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source) // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web // module @. object Parsers extends RegexParsers { /* white space and comments */ override val whiteSpace = "".r private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE) private val spaces = rep(space) /* ignored text */ private val ignored: Parser[Chunk] = rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ { case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) } private def ignored_line: Parser[(Chunk, Line_Context)] = ignored ^^ { case a => (a, Ignored) } /* delimited string: outermost "..." or {...} and body with balanced {...} */ // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] = new Parser[(String, Delimited)] { - require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0) + require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0, + "bad delimiter depth") def apply(in: Input) = { val start = in.offset val end = in.source.length var i = start var q = delim.quoted var d = delim.depth var finished = false while (!finished && i < end) { val c = in.source.charAt(i) if (c == '"' && d == 0) { i += 1; d = 1; q = true } else if (c == '"' && d == 1 && q) { i += 1; d = 0; q = false; finished = true } else if (c == '{') { i += 1; d += 1 } else if (c == '}') { if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true } else {i = start; finished = true } } else if (d > 0) i += 1 else finished = true } if (i == start) Failure("bad input", in) else { val s = in.source.subSequence(start, i).toString Success((s, Delimited(q, d)), in.drop(i - start)) } } }.named("delimited_depth") private def delimited: Parser[Token] = delimited_depth(Closed) ^? { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) } private def recover_delimited: Parser[Token] = """["{][^@]*""".r ^^ token(Token.Kind.ERROR) def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] = delimited_depth(ctxt.delim) ^^ { case (s, delim1) => (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } | recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) } /* other tokens */ private val at = "@" ^^ keyword private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT) private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME) private val identifier = """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r private val ident = identifier ^^ token(Token.Kind.IDENT) val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space)) /* body */ private val body = delimited | (recover_delimited | other_token) private def body_line(ctxt: Item) = if (ctxt.delim.depth > 0) delimited_line(ctxt) else delimited_line(ctxt) | other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } | ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) } /* items: command or entry */ private val item_kind = identifier ^^ { case a => val kind = if (is_command(a)) Token.Kind.COMMAND else if (is_entry(a)) Token.Kind.ENTRY else Token.Kind.IDENT Token(kind, a) } private val item_begin = "{" ^^ { case a => ("}", keyword(a)) } | "(" ^^ { case a => (")", keyword(a)) } private def item_name(kind: String) = kind.toLowerCase match { case "preamble" => failure("") case "string" => identifier ^^ token(Token.Kind.NAME) case _ => name } private val item_start = at ~ spaces ~ item_kind ~ spaces ^^ { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) } private val item: Parser[Chunk] = (item_start ~ item_begin ~ spaces) into { case (kind, a) ~ ((end, b)) ~ c => opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ { case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } } private val recover_item: Parser[Chunk] = at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) } /* chunks */ val chunk: Parser[Chunk] = ignored | (item | recover_item) def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = { ctxt match { case Ignored => ignored_line | at ^^ { case a => (Chunk("", List(a)), At) } case At => space ^^ { case a => (Chunk("", List(a)), ctxt) } | item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } | recover_item ^^ { case a => (a, Ignored) } | ignored_line case Item_Start(kind) => space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } | recover_item ^^ { case a => (a, Ignored) } | ignored_line case Item_Open(kind, end) => space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } | body_line(Item(kind, end, Closed)) | ignored_line case item_ctxt: Item => body_line(item_ctxt) | ignored_line case _ => failure("") } } } /* parse */ def parse(input: CharSequence): List[Chunk] = Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match { case Parsers.Success(result, _) => result case _ => error("Unexpected failure to parse input:\n" + input.toString) } def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = { var in: Reader[Char] = Scan.char_reader(input) val chunks = new mutable.ListBuffer[Chunk] var ctxt = context while (!in.atEnd) { Parsers.parse(Parsers.chunk_line(ctxt), in) match { case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest case Parsers.NoSuccess(_, rest) => error("Unepected failure to parse input:\n" + rest.source.toString) } } (chunks.toList, ctxt) } /** HTML output **/ private val output_styles = List( "" -> "html-n", "plain" -> "html-n", "alpha" -> "html-a", "named" -> "html-n", "paragraph" -> "html-n", "unsort" -> "html-u", "unsortlist" -> "html-u") def html_output(bib: List[Path], title: String = "Bibliography", body: Boolean = false, citations: List[String] = List("*"), style: String = "", chronological: Boolean = false): String = { Isabelle_System.with_tmp_dir("bibtex")(tmp_dir => { /* database files */ val bib_files = bib.map(_.drop_ext) val bib_names = { val names0 = bib_files.map(_.file_name) if (Library.duplicates(names0).isEmpty) names0 else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name }) } for ((a, b) <- bib_files zip bib_names) { File.copy(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib")) } /* style file */ val bst = output_styles.toMap.get(style) match { case Some(base) => base + (if (chronological) "c" else "") + ".bst" case None => error("Bad style for bibtex HTML output: " + quote(style) + "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")") } File.copy(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir) /* result */ val in_file = Path.explode("bib.aux") val out_file = Path.explode("bib.html") File.write(tmp_dir + in_file, bib_names.mkString("\\bibdata{", ",", "}\n") + citations.map(cite => "\\citation{" + cite + "}\n").mkString) Isabelle_System.bash( "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" + " -u -s " + Bash.string(proper_string(style) getOrElse "empty") + (if (chronological) " -c" else "") + (if (title != "") " -h " + Bash.string(title) + " " else "") + " " + File.bash_path(in_file) + " " + File.bash_path(out_file), cwd = tmp_dir.file).check val html = File.read(tmp_dir + out_file) if (body) { cat_lines( split_lines(html). dropWhile(line => !line.startsWith("

", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\