diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,502 +1,502 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Miscellaneous Isabelle system operations. */ package isabelle import java.util.{Map => JMap, HashMap} import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes import scala.jdk.CollectionConverters._ object Isabelle_System { /* settings environment */ def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = { val env0 = isabelle.setup.Environment.settings() if (putenv.isEmpty) env0 else { val env = new HashMap(env0) for ((a, b) <- putenv) env.put(a, b) env } } def getenv(name: String, env: JMap[String, String] = settings()): String = Option(env.get(name)).getOrElse("") def getenv_strict(name: String, env: JMap[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) /* services */ abstract class Service @volatile private var _services: Option[List[Class[Service]]] = None def services(): List[Class[Service]] = { if (_services.isEmpty) init() // unsynchronized check _services.get } def make_services[C](c: Class[C]): List[C] = for { c1 <- services() if Library.is_subclass(c1, c) } yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C] /* init settings + services */ def make_services(): List[Class[Service]] = { def make(where: String, names: List[String]): List[Class[Service]] = { for (name <- names) yield { def err(msg: String): Nothing = error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg) try { Class.forName(name).asInstanceOf[Class[Service]] } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } } def from_env(variable: String): List[Class[Service]] = make(quote(variable), space_explode(':', getenv_strict(variable))) def from_jar(platform_jar: String): List[Class[Service]] = make(quote(platform_jar), isabelle.setup.Build.get_services(JPath.of(platform_jar)).asScala.toList) from_env("ISABELLE_SCALA_SERVICES") ::: Scala.class_path().flatMap(from_jar) } def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = { isabelle.setup.Environment.init(isabelle_root, cygwin_root) synchronized { if (_services.isEmpty) { _services = Some(make_services()) } } } /* getetc -- static distribution parameters */ def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] = { val path = root + Path.basic("etc") + Path.basic(name) if (path.is_file) { Library.trim_split_lines(File.read(path)) match { case Nil => None case List(s) => Some(s) case _ => error("Single line expected in " + path.absolute) } } else None } /* Isabelle distribution identification */ def isabelle_id(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse { if (Mercurial.is_repository(root)) Mercurial.repository(root).parent() else error("Failed to identify Isabelle distribution " + root.expand) } object Isabelle_Id extends Scala.Fun_String("isabelle_id") { val here = Scala_Project.here def apply(arg: String): String = isabelle_id() } def isabelle_tags(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse { if (Mercurial.is_repository(root)) { val hg = Mercurial.repository(root) hg.tags(rev = hg.parent()) } else "" } def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER")) def isabelle_heading(): String = isabelle_identifier() match { case None => "" case Some(version) => " (" + version + ")" } def isabelle_name(): String = getenv_strict("ISABELLE_NAME") def identification(): String = "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading() /** file-system operations **/ /* scala functions */ private def apply_paths( args: List[String], fun: PartialFunction[List[Path], Unit] ): List[String] = { fun(args.map(Path.explode)) Nil } private def apply_paths1(args: List[String], fun: Path => Unit): List[String] = apply_paths(args, { case List(path) => fun(path) }) private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2) => fun(path1, path2) }) private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def make_directory(path: Path): Path = { if (!path.is_dir) { try { Files.createDirectories(path.java_path) } catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } } path } def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path) def copy_dir(dir1: Path, dir2: Path): Unit = { val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)) if (!res.ok) { cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err) } } def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = { if (dir2.is_file || dir2.is_dir) error("Directory already exists: " + dir2.absolute) else { try { copy_dir(dir1, dir2); body } finally { rm_tree(dir2 ) } } } object Make_Directory extends Scala.Fun_Strings("make_directory") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, make_directory) } object Copy_Dir extends Scala.Fun_Strings("copy_dir") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir) } /* copy files */ def copy_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) { try { Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } catch { case ERROR(msg) => cat_error("Failed to copy file " + File.path(src).absolute + " to " + File.path(dst).absolute, msg) } } } def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file) def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = { val src1 = src.expand val src1_dir = src1.dir if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory") copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir)) } object Copy_File extends Scala.Fun_Strings("copy_file") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_file) } object Copy_File_Base extends Scala.Fun_Strings("copy_file_base") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base) } /* move files */ def move_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file) /* symbolic link */ def symlink(src: Path, dst: Path, force: Boolean = false, native: Boolean = false): Unit = { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete def cygwin_link(): Unit = { if (native) { error("Failed to create native symlink on Windows: " + quote(src_file.toString) + "\n(but it could work as Administrator)") } else isabelle.setup.Environment.cygwin_link(File.standard_path(src), target) } try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => cygwin_link() case _: FileSystemException if Platform.is_windows => cygwin_link() } } /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit() file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile): Unit = { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def rm_tree(root: Path): Unit = rm_tree(root.file) object Rm_Tree extends Scala.Fun_Strings("rm_tree") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree) } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit() dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit): Unit = { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) move_file(dir, old_dir) move_file(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* GNU bash */ def bash(script: String, description: String = "", cwd: JFile = null, env: JMap[String, String] = settings(), redirect: Boolean = false, input: String = "", progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Bash.Watchdog] = None, strict: Boolean = true, cleanup: () => Unit = () => () ): Process_Result = { Bash.process(script, description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } /* command-line tools */ def require_command(cmd: String, test: String = "--version"): Unit = { if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd)) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, strip: Int = 0, redirect: Boolean = false ): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") + (if (strip <= 0) "" else "--strip-components=" + strip + " ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = { with_tmp_file("patch") { patch => Isabelle_System.bash( "diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) + " > " + File.bash_path(patch), cwd = base_dir.file).check_rc(_ <= 1) File.read(patch) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def open_external_file(name: String): Boolean = { val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString val external = ext.nonEmpty && Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext) if (external) { if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name)) else open(name) } external } /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => getenv_strict("ISABELLE_LOGIC") } } /* download file */ def download(url_name: String, progress: Progress = new Progress): HTTP.Content = { val url = Url(url_name) progress.echo("Getting " + quote(url_name)) try { HTTP.Client.get(url) } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) } } def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = Bytes.write(file, download(url_name, progress = progress).bytes) object Download extends Scala.Fun("download", thread = true) { val here = Scala_Project.here override def invoke(args: List[Bytes]): List[Bytes] = - args match { case List(url) => List(download(url.text).bytes) case _ => ??? } + args.map(url => download(url.text).bytes) } /* repositories */ val isabelle_repository: Mercurial.Server = Mercurial.Server("https://isabelle.sketis.net/repos/isabelle") val afp_repository: Mercurial.Server = Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel") def official_releases(): List[String] = Library.trim_split_lines( isabelle_repository.read_file(Path.explode("Admin/Release/official"))) } diff --git a/src/Tools/Graphview/layout.scala b/src/Tools/Graphview/layout.scala --- a/src/Tools/Graphview/layout.scala +++ b/src/Tools/Graphview/layout.scala @@ -1,422 +1,422 @@ /* Title: Tools/Graphview/layout.scala Author: Markus Kaiser, TU Muenchen Author: Makarius DAG layout according to: Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing, DIMACS International Workshop (GD'94), Springer LNCS 894, 1995. https://doi.org/10.1007/3-540-58950-3_371 ftp://ftp.cs.uni-sb.de/pub/graphics/vcg/doc/tr-A03-94.ps.gz */ package isabelle.graphview import isabelle._ object Layout { /* graph structure */ object Vertex { object Ordering extends scala.math.Ordering[Vertex] { def compare(v1: Vertex, v2: Vertex): Int = (v1, v2) match { case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b) case (Dummy(a1, a2, i), Dummy(b1, b2, j)) => Graph_Display.Node.Ordering.compare(a1, b1) match { case 0 => Graph_Display.Node.Ordering.compare(a2, b2) match { case 0 => i compare j case ord => ord } case ord => ord } case (Node(a), Dummy(b, _, _)) => Graph_Display.Node.Ordering.compare(a, b) match { case 0 => -1 case ord => ord } case (Dummy(a, _, _), Node(b)) => Graph_Display.Node.Ordering.compare(a, b) match { case 0 => 1 case ord => ord } } } } sealed abstract class Vertex case class Node(node: Graph_Display.Node) extends Vertex case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex sealed case class Info( x: Double, y: Double, width2: Double, height2: Double, lines: List[String] ) { def left: Double = x - width2 def right: Double = x + width2 def width: Double = 2 * width2 def height: Double = 2 * height2 } type Graph = isabelle.Graph[Vertex, Info] def make_graph(entries: List[((Vertex, Info), List[Vertex])]): Graph = isabelle.Graph.make(entries)(Vertex.Ordering) val empty_graph: Graph = make_graph(Nil) /* vertex x coordinate */ private def vertex_left(graph: Graph, v: Vertex) = graph.get_node(v).left private def vertex_right(graph: Graph, v: Vertex) = graph.get_node(v).right private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph = if (dx == 0.0) graph else graph.map_node(v, info => info.copy(x = info.x + dx)) /* layout */ val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph) private type Levels = Map[Vertex, Int] private val empty_levels: Levels = Map.empty def make( options: Options, metrics: Metrics, node_text: (Graph_Display.Node, XML.Body) => String, input_graph: Graph_Display.Graph ): Layout = { if (input_graph.is_empty) empty else { /* initial graph */ val initial_graph = make_graph( input_graph.iterator.map( { case (a, (content, (_, bs))) => val lines = split_lines(node_text(a, content)) val w2 = metrics.node_width2(lines) val h2 = metrics.node_height2(lines.length) ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node.apply)) }).toList) val initial_levels: Levels = initial_graph.topological_order.foldLeft(empty_levels) { case (levels, vertex) => val level = 1 + initial_graph.imm_preds(vertex).foldLeft(-1) { case (m, v) => m max levels(v) } levels + (vertex -> level) } /* graph with dummies */ val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil) val (dummy_graph, dummy_levels) = input_graph.edges_iterator.foldLeft((initial_graph, initial_levels)) { case ((graph, levels), (node1, node2)) => val v1 = Node(node1); val l1 = levels(v1) val v2 = Node(node2); val l2 = levels(v2) if (l2 - l1 <= 1) (graph, levels) else { val dummies_levels = (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex } yield (Dummy(node1, node2, i), l)).toList val dummies = dummies_levels.map(_._1) val levels1 = dummies_levels.foldLeft(levels)(_ + _) val graph1 = (v1 :: dummies ::: List(v2)).sliding(2) .foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) { case (g, Seq(a, b)) => g.add_edge(a, b) - case _ => ??? + case (g, _) => g } (graph1, levels1) } } /* minimize edge crossings and initial coordinates */ val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels)) val levels_graph: Graph = levels.foldLeft((dummy_graph, 0.0)) { case ((graph, y), level) => val num_lines = level.foldLeft(0) { case (n, v) => n max graph.get_node(v).lines.length } val num_edges = level.foldLeft(0) { case (n, v) => n + graph.imm_succs(v).size } val y1 = y + metrics.node_height2(num_lines) val graph1 = level.foldLeft((graph, 0.0)) { case ((g, x), v) => val info = g.get_node(v) val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1)) val x1 = x + info.width + metrics.gap (g1, x1) }._1 val y2 = y1 + metrics.level_height2(num_lines, num_edges) (graph1, y2) }._1 /* pendulum/rubberband layout */ val output_graph = rubberband(options, metrics, levels, pendulum(options, metrics, levels, levels_graph)) new Layout(metrics, input_graph, output_graph) } } /** edge crossings **/ private type Level = List[Vertex] private def minimize_crossings( options: Options, graph: Graph, levels: List[Level] ): List[Level] = { def resort(parent: Level, child: Level, top_down: Boolean): Level = child.map({ v => val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v) val weight = ps.foldLeft(0.0) { case (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) (v, weight) }).sortBy(_._2).map(_._1) (1 to (2 * options.int("graphview_iterations_minimize_crossings"))). foldLeft((levels, count_crossings(graph, levels))) { case ((old_levels, old_crossings), iteration) => val top_down = (iteration % 2 == 1) val new_levels = if (top_down) { old_levels.tail.foldLeft(List(old_levels.head)) { case (tops, bot) => resort(tops.head, bot, top_down) :: tops }.reverse } else { val rev_old_levels = old_levels.reverse rev_old_levels.tail.foldLeft(List(rev_old_levels.head)) { case (bots, top) => resort(bots.head, top, top_down) :: bots } } val new_crossings = count_crossings(graph, new_levels) if (new_crossings < old_crossings) (new_levels, new_crossings) else (old_levels, old_crossings) }._1 } private def level_list(levels: Levels): List[Level] = { val max_lev = levels.foldLeft(-1) { case (m, (_, l)) => m max l } val buckets = new Array[Level](max_lev + 1) for (l <- 0 to max_lev) { buckets(l) = Nil } for ((v, l) <- levels) { buckets(l) = v :: buckets(l) } buckets.iterator.map(_.sorted(Vertex.Ordering)).toList } private def count_crossings(graph: Graph, levels: List[Level]): Int = levels.iterator.sliding(2).map { case Seq(top, bot) => top.iterator.zipWithIndex.map { case (outer_parent, outer_parent_index) => graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child => (0 until outer_parent_index).iterator.map(inner_parent => graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)) .count(inner_child => outer_child < inner_child)).sum).sum }.sum case _ => 0 }.sum /** pendulum method **/ /*This is an auxiliary class which is used by the layout algorithm when calculating coordinates with the "pendulum method". A "region" is a group of vertices which "stick together".*/ private class Region(val content: List[Vertex]) { def distance(metrics: Metrics, graph: Graph, that: Region): Double = vertex_left(graph, that.content.head) - vertex_right(graph, this.content.last) - metrics.gap def deflection(graph: Graph, top_down: Boolean): Double = ((for (a <- content.iterator) yield { val x = graph.get_node(a).x val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a) bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1) }).sum / content.length).round.toDouble def move(graph: Graph, dx: Double): Graph = if (dx == 0.0) graph else content.foldLeft(graph)(move_vertex(_, _, dx)) def combine(that: Region): Region = new Region(content ::: that.content) } private def pendulum( options: Options, metrics: Metrics, levels: List[Level], levels_graph: Graph ): Graph = { def combine_regions(graph: Graph, top_down: Boolean, level: List[Region]): List[Region] = level match { case r1 :: rest => val rest1 = combine_regions(graph, top_down, rest) rest1 match { case r2 :: rest2 => val d1 = r1.deflection(graph, top_down) val d2 = r2.deflection(graph, top_down) if (// Do regions touch? r1.distance(metrics, graph, r2) <= 0.0 && // Do they influence each other? (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0)) r1.combine(r2) :: rest2 else r1 :: rest1 case _ => r1 :: rest1 } case _ => level } def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) = { level.indices.foldLeft((graph, false)) { case ((graph, moved), i) => val r = level(i) val d = r.deflection(graph, top_down) val dx = if (d < 0.0 && i > 0) { - (level(i - 1).distance(metrics, graph, r) min (- d)) } else if (d >= 0.0 && i < level.length - 1) { r.distance(metrics, graph, level(i + 1)) min d } else d (r.move(graph, dx), moved || d != 0.0) } } val initial_regions = levels.map(level => level.map(l => new Region(List(l)))) (1 to (2 * options.int("graphview_iterations_pendulum"))). foldLeft((levels_graph, initial_regions, true)) { case ((graph, regions, moved), iteration) => val top_down = (iteration % 2 == 1) if (moved) { val (graph1, regions1, moved1) = (if (top_down) regions else regions.reverse). foldLeft((graph, List.empty[List[Region]], false)) { case ((graph, tops, moved), bot) => val bot1 = combine_regions(graph, top_down, bot) val (graph1, moved1) = deflect(bot1, top_down, graph) (graph1, bot1 :: tops, moved || moved1) } (graph1, regions1.reverse, moved1) } else (graph, regions, moved) }._1 } /** rubberband method **/ private def force_weight(graph: Graph, v: Vertex): Double = { val preds = graph.imm_preds(v) val succs = graph.imm_succs(v) val n = preds.size + succs.size if (n == 0) 0.0 else { val x = graph.get_node(v).x ((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n } } private def rubberband( options: Options, metrics: Metrics, levels: List[Level], graph: Graph ): Graph = { val gap = metrics.gap (1 to (2 * options.int("graphview_iterations_rubberband"))).foldLeft(graph) { case (graph, _) => levels.foldLeft(graph) { case (graph, level) => val m = level.length - 1 level.iterator.zipWithIndex.foldLeft(graph) { case (g, (v, i)) => val d = force_weight(g, v) if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) || d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d)) move_vertex(g, v, d.round.toDouble) else g } } } } } final class Layout private( val metrics: Metrics, val input_graph: Graph_Display.Graph, val output_graph: Layout.Graph ) { /* vertex coordinates */ def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout = { if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this else { val output_graph1 = output_graph.map_node(v, info => info.copy(x = info.x + dx, y = info.y + dy)) new Layout(metrics, input_graph, output_graph1) } } /* regular nodes */ def get_node(node: Graph_Display.Node): Layout.Info = output_graph.get_node(Layout.Node(node)) def nodes_iterator: Iterator[Layout.Info] = for ((_: Layout.Node, (info, _)) <- output_graph.iterator) yield info /* dummies */ def dummies_iterator: Iterator[Layout.Info] = for ((_: Layout.Dummy, (info, _)) <- output_graph.iterator) yield info def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Info] = new Iterator[Layout.Info] { private var index = 0 def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index)) def next(): Layout.Info = { val info = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index)) index += 1 info } } } diff --git a/src/Tools/Graphview/shapes.scala b/src/Tools/Graphview/shapes.scala --- a/src/Tools/Graphview/shapes.scala +++ b/src/Tools/Graphview/shapes.scala @@ -1,215 +1,215 @@ /* Title: Tools/Graphview/shapes.scala Author: Markus Kaiser, TU Muenchen Author: Makarius Drawable shapes. */ package isabelle.graphview import isabelle._ import java.awt.{BasicStroke, Graphics2D, Shape} import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, RoundRectangle2D, PathIterator} object Shapes { private val default_stroke = new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) def shape(info: Layout.Info): Rectangle2D.Double = new Rectangle2D.Double(info.x - info.width2, info.y - info.height2, info.width, info.height) def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node): Unit = { val metrics = graphview.metrics val extra = metrics.char_width val info = graphview.layout.get_node(node) gfx.setColor(graphview.highlight_color) gfx.fill(new Rectangle2D.Double( info.x - info.width2 - extra, info.y - info.height2 - extra, info.width + 2 * extra, info.height + 2 * extra)) } def paint_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node): Unit = { val metrics = graphview.metrics val info = graphview.layout.get_node(node) val c = graphview.node_color(node) val s = shape(info) gfx.setColor(c.background) gfx.fill(s) gfx.setColor(c.border) gfx.setStroke(default_stroke) gfx.draw(s) gfx.setColor(c.foreground) gfx.setFont(metrics.font) val text_width = info.lines.foldLeft(0.0) { case (w, line) => w max metrics.string_bounds(line).getWidth } val text_height = (info.lines.length max 1) * metrics.height.ceil val x = (s.getCenterX - text_width / 2).round.toInt var y = (s.getCenterY - text_height / 2 + metrics.ascent).round.toInt for (line <- info.lines) { gfx.drawString(Word.bidi_override(line), x, y) y += metrics.height.ceil.toInt } } def paint_dummy(gfx: Graphics2D, graphview: Graphview, info: Layout.Info): Unit = { gfx.setStroke(default_stroke) gfx.setColor(graphview.dummy_color) gfx.draw(shape(info)) } object Straight_Edge { def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge): Unit = { val p = graphview.layout.get_node(edge._1) val q = graphview.layout.get_node(edge._2) val ds = { val a = p.y min q.y val b = p.y max q.y graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList } val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) path.moveTo(p.x, p.y) ds.foreach(d => path.lineTo(d.x, d.y)) path.lineTo(q.x, q.y) if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _)) gfx.setStroke(default_stroke) gfx.setColor(graphview.edge_color(edge, p.y < q.y)) gfx.draw(path) if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) } } object Cardinal_Spline_Edge { private val slack = 0.1 def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge): Unit = { val p = graphview.layout.get_node(edge._1) val q = graphview.layout.get_node(edge._2) val ds = { val a = p.y min q.y val b = p.y max q.y graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList } if (ds.isEmpty) Straight_Edge.paint(gfx, graphview, edge) else { val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) path.moveTo(p.x, p.y) val coords = p :: ds ::: List(q) val dx = coords(2).x - coords(0).x val dy = coords(2).y - coords(0).y val (dx2, dy2) = coords.sliding(3).foldLeft((dx, dy)) { case ((dx, dy), Seq(l, m, r)) => val dx2 = r.x - l.x val dy2 = r.y - l.y path.curveTo( l.x + slack * dx, l.y + slack * dy, m.x - slack * dx2, m.y - slack * dy2, m.x, m.y) (dx2, dy2) - case _ => ??? + case (p, _) => p } val l = ds.last path.curveTo( l.x + slack * dx2, l.y + slack * dy2, q.x - slack * dx2, q.y - slack * dy2, q.x, q.y) if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _)) gfx.setStroke(default_stroke) gfx.setColor(graphview.edge_color(edge, p.y < q.y)) gfx.draw(path) if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) } } } object Arrow_Head { type Point = (Double, Double) private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] = { def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] = { val i = path.getPathIterator(null, 1.0) val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0) var p1 = (0.0, 0.0) var p2 = (0.0, 0.0) while (!i.isDone) { i.currentSegment(seg) match { case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1)) case PathIterator.SEG_LINETO => p1 = p2 p2 = (seg(0), seg(1)) if(shape.contains(seg(0), seg(1))) return Some((p1, p2)) case _ => } i.next() } None } def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] = { val ((fx, fy), (tx, ty)) = line if (shape.contains(fx, fy) == shape.contains(tx, ty)) None else { val (dx, dy) = (fx - tx, fy - ty) if ((dx * dx + dy * dy) < 1.0) { val at = AffineTransform.getTranslateInstance(fx, fy) at.rotate(- (math.atan2(dx, dy) + math.Pi / 2)) Some(at) } else { val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0) if (shape.contains(fx, fy) == shape.contains(mx, my)) binary_search(((mx, my), (tx, ty)), shape) else binary_search(((fx, fy), (mx, my)), shape) } } } intersecting_line(path, shape) match { case None => None case Some(line) => binary_search(line, shape) } } def paint(gfx: Graphics2D, path: GeneralPath, shape: Shape): Unit = { position(path, shape) match { case None => case Some(at) => val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3) arrow.moveTo(0, 0) arrow.lineTo(-10, 4) arrow.lineTo(-6, 0) arrow.lineTo(-10, -4) arrow.lineTo(0, 0) arrow.transform(at) gfx.fill(arrow) } } } }