diff --git a/etc/build.props b/etc/build.props --- a/etc/build.props +++ b/etc/build.props @@ -1,307 +1,308 @@ title = Isabelle/Scala module = $ISABELLE_HOME/lib/classes/isabelle.jar main = isabelle.jedit.JEdit_Main resources = \ lib/services/java.nio.charset.spi.CharsetProvider:META-INF/services/ \ lib/logo/isabelle_transparent-32.gif:isabelle/ \ lib/logo/isabelle_transparent.gif:isabelle/ sources = \ src/HOL/SPARK/Tools/spark.scala \ src/HOL/Tools/ATP/system_on_tptp.scala \ src/HOL/Tools/Mirabelle/mirabelle.scala \ src/HOL/Tools/Nitpick/kodkod.scala \ src/Pure/Admin/afp.scala \ src/Pure/Admin/build_csdp.scala \ src/Pure/Admin/build_cygwin.scala \ src/Pure/Admin/build_doc.scala \ src/Pure/Admin/build_e.scala \ src/Pure/Admin/build_fonts.scala \ src/Pure/Admin/build_history.scala \ src/Pure/Admin/build_jcef.scala \ src/Pure/Admin/build_jdk.scala \ src/Pure/Admin/build_jedit.scala \ src/Pure/Admin/build_log.scala \ src/Pure/Admin/build_minisat.scala \ src/Pure/Admin/build_pdfjs.scala \ src/Pure/Admin/build_polyml.scala \ src/Pure/Admin/build_release.scala \ src/Pure/Admin/build_scala.scala \ src/Pure/Admin/build_spass.scala \ src/Pure/Admin/build_sqlite.scala \ src/Pure/Admin/build_status.scala \ src/Pure/Admin/build_vampire.scala \ src/Pure/Admin/build_verit.scala \ src/Pure/Admin/build_zipperposition.scala \ src/Pure/Admin/check_sources.scala \ src/Pure/Admin/ci_build_benchmark.scala \ src/Pure/Admin/ci_profile.scala \ src/Pure/Admin/isabelle_cronjob.scala \ src/Pure/Admin/isabelle_devel.scala \ src/Pure/Admin/jenkins.scala \ src/Pure/Admin/other_isabelle.scala \ src/Pure/Concurrent/consumer_thread.scala \ src/Pure/Concurrent/counter.scala \ src/Pure/Concurrent/delay.scala \ src/Pure/Concurrent/event_timer.scala \ src/Pure/Concurrent/future.scala \ src/Pure/Concurrent/isabelle_thread.scala \ src/Pure/Concurrent/mailbox.scala \ src/Pure/Concurrent/par_list.scala \ src/Pure/Concurrent/synchronized.scala \ src/Pure/GUI/color_value.scala \ src/Pure/GUI/desktop_app.scala \ src/Pure/GUI/gui.scala \ src/Pure/GUI/gui_thread.scala \ src/Pure/GUI/popup.scala \ src/Pure/GUI/wrap_panel.scala \ src/Pure/General/antiquote.scala \ src/Pure/General/base64.scala \ src/Pure/General/bytes.scala \ src/Pure/General/cache.scala \ src/Pure/General/codepoint.scala \ src/Pure/General/comment.scala \ src/Pure/General/completion.scala \ src/Pure/General/csv.scala \ src/Pure/General/date.scala \ src/Pure/General/exn.scala \ src/Pure/General/file.scala \ src/Pure/General/file_watcher.scala \ src/Pure/General/graph.scala \ src/Pure/General/graph_display.scala \ src/Pure/General/graphics_file.scala \ src/Pure/General/http.scala \ src/Pure/General/json.scala \ src/Pure/General/json_api.scala \ src/Pure/General/linear_set.scala \ src/Pure/General/logger.scala \ src/Pure/General/long_name.scala \ src/Pure/General/mailman.scala \ src/Pure/General/mercurial.scala \ src/Pure/General/multi_map.scala \ src/Pure/General/output.scala \ src/Pure/General/path.scala \ src/Pure/General/position.scala \ src/Pure/General/pretty.scala \ src/Pure/General/properties.scala \ src/Pure/General/rdf.scala \ src/Pure/General/rsync.scala \ src/Pure/General/scan.scala \ src/Pure/General/sha1.scala \ src/Pure/General/sql.scala \ src/Pure/General/ssh.scala \ src/Pure/General/symbol.scala \ src/Pure/General/time.scala \ src/Pure/General/timing.scala \ src/Pure/General/untyped.scala \ src/Pure/General/url.scala \ src/Pure/General/utf8.scala \ src/Pure/General/uuid.scala \ src/Pure/General/value.scala \ src/Pure/General/word.scala \ src/Pure/General/xz.scala \ src/Pure/Isar/document_structure.scala \ src/Pure/Isar/keyword.scala \ src/Pure/Isar/line_structure.scala \ src/Pure/Isar/outer_syntax.scala \ src/Pure/Isar/parse.scala \ src/Pure/Isar/token.scala \ src/Pure/ML/ml_console.scala \ src/Pure/ML/ml_lex.scala \ src/Pure/ML/ml_process.scala \ src/Pure/ML/ml_profiling.scala \ src/Pure/ML/ml_statistics.scala \ src/Pure/ML/ml_syntax.scala \ src/Pure/PIDE/byte_message.scala \ src/Pure/PIDE/command.scala \ src/Pure/PIDE/command_span.scala \ src/Pure/PIDE/document.scala \ src/Pure/PIDE/document_id.scala \ src/Pure/PIDE/document_status.scala \ src/Pure/PIDE/editor.scala \ src/Pure/PIDE/headless.scala \ src/Pure/PIDE/line.scala \ src/Pure/PIDE/markup.scala \ src/Pure/PIDE/markup_tree.scala \ src/Pure/PIDE/protocol.scala \ src/Pure/PIDE/protocol_handlers.scala \ src/Pure/PIDE/protocol_message.scala \ src/Pure/PIDE/prover.scala \ src/Pure/PIDE/query_operation.scala \ src/Pure/PIDE/rendering.scala \ src/Pure/PIDE/resources.scala \ src/Pure/PIDE/session.scala \ src/Pure/PIDE/text.scala \ src/Pure/PIDE/xml.scala \ src/Pure/PIDE/yxml.scala \ src/Pure/ROOT.scala \ src/Pure/System/bash.scala \ src/Pure/System/classpath.scala \ src/Pure/System/command_line.scala \ src/Pure/System/components.scala \ src/Pure/System/executable.scala \ src/Pure/System/getopts.scala \ src/Pure/System/isabelle_charset.scala \ src/Pure/System/isabelle_fonts.scala \ src/Pure/System/isabelle_platform.scala \ src/Pure/System/isabelle_process.scala \ src/Pure/System/isabelle_system.scala \ src/Pure/System/isabelle_tool.scala \ src/Pure/System/java_statistics.scala \ src/Pure/System/linux.scala \ src/Pure/System/mingw.scala \ src/Pure/System/numa.scala \ src/Pure/System/options.scala \ src/Pure/System/platform.scala \ src/Pure/System/posix_interrupt.scala \ src/Pure/System/process_result.scala \ src/Pure/System/progress.scala \ src/Pure/System/scala.scala \ src/Pure/System/system_channel.scala \ src/Pure/System/tty_loop.scala \ src/Pure/Thy/bibtex.scala \ src/Pure/Thy/document_build.scala \ src/Pure/Thy/export.scala \ src/Pure/Thy/export_theory.scala \ src/Pure/Thy/file_format.scala \ src/Pure/Thy/html.scala \ src/Pure/Thy/latex.scala \ src/Pure/Thy/presentation.scala \ src/Pure/Thy/sessions.scala \ src/Pure/Thy/thy_element.scala \ src/Pure/Thy/thy_header.scala \ src/Pure/Thy/thy_syntax.scala \ src/Pure/Tools/build.scala \ src/Pure/Tools/build_docker.scala \ src/Pure/Tools/build_job.scala \ src/Pure/Tools/check_keywords.scala \ src/Pure/Tools/debugger.scala \ src/Pure/Tools/doc.scala \ src/Pure/Tools/dump.scala \ src/Pure/Tools/flarum.scala \ src/Pure/Tools/fontforge.scala \ src/Pure/Tools/java_monitor.scala \ src/Pure/Tools/logo.scala \ src/Pure/Tools/mkroot.scala \ src/Pure/Tools/phabricator.scala \ src/Pure/Tools/print_operation.scala \ src/Pure/Tools/profiling_report.scala \ src/Pure/Tools/scala_build.scala \ src/Pure/Tools/scala_project.scala \ src/Pure/Tools/server.scala \ src/Pure/Tools/server_commands.scala \ src/Pure/Tools/simplifier_trace.scala \ src/Pure/Tools/spell_checker.scala \ src/Pure/Tools/sync.scala \ src/Pure/Tools/task_statistics.scala \ src/Pure/Tools/update.scala \ src/Pure/Tools/update_cartouches.scala \ src/Pure/Tools/update_comments.scala \ src/Pure/Tools/update_header.scala \ src/Pure/Tools/update_then.scala \ src/Pure/Tools/update_theorems.scala \ src/Pure/library.scala \ src/Pure/pure_thy.scala \ src/Pure/term.scala \ src/Pure/term_xml.scala \ src/Pure/thm_name.scala \ src/Tools/Graphview/graph_file.scala \ src/Tools/Graphview/graph_panel.scala \ src/Tools/Graphview/graphview.scala \ src/Tools/Graphview/layout.scala \ src/Tools/Graphview/main_panel.scala \ src/Tools/Graphview/metrics.scala \ src/Tools/Graphview/model.scala \ src/Tools/Graphview/mutator.scala \ src/Tools/Graphview/mutator_dialog.scala \ src/Tools/Graphview/mutator_event.scala \ src/Tools/Graphview/popups.scala \ src/Tools/Graphview/shapes.scala \ src/Tools/Graphview/tree_panel.scala \ src/Tools/VSCode/src/build_vscode_extension.scala \ src/Tools/VSCode/src/build_vscodium.scala \ src/Tools/VSCode/src/channel.scala \ src/Tools/VSCode/src/dynamic_output.scala \ src/Tools/VSCode/src/language_server.scala \ src/Tools/VSCode/src/lsp.scala \ src/Tools/VSCode/src/preview_panel.scala \ src/Tools/VSCode/src/state_panel.scala \ src/Tools/VSCode/src/vscode_main.scala \ src/Tools/VSCode/src/vscode_model.scala \ src/Tools/VSCode/src/vscode_rendering.scala \ src/Tools/VSCode/src/vscode_resources.scala \ src/Tools/VSCode/src/vscode_spell_checker.scala \ src/Tools/jEdit/src/active.scala \ src/Tools/jEdit/src/base_plugin.scala \ src/Tools/jEdit/src/completion_popup.scala \ src/Tools/jEdit/src/context_menu.scala \ src/Tools/jEdit/src/debugger_dockable.scala \ src/Tools/jEdit/src/dockable.scala \ + src/Tools/jEdit/src/document_dockable.scala \ src/Tools/jEdit/src/document_model.scala \ src/Tools/jEdit/src/document_view.scala \ src/Tools/jEdit/src/documentation_dockable.scala \ src/Tools/jEdit/src/fold_handling.scala \ src/Tools/jEdit/src/font_info.scala \ src/Tools/jEdit/src/graphview_dockable.scala \ src/Tools/jEdit/src/info_dockable.scala \ src/Tools/jEdit/src/isabelle.scala \ src/Tools/jEdit/src/isabelle_encoding.scala \ src/Tools/jEdit/src/isabelle_export.scala \ src/Tools/jEdit/src/isabelle_options.scala \ src/Tools/jEdit/src/isabelle_session.scala \ src/Tools/jEdit/src/isabelle_vfs.scala \ src/Tools/jEdit/src/jedit_bibtex.scala \ src/Tools/jEdit/src/jedit_editor.scala \ src/Tools/jEdit/src/jedit_lib.scala \ src/Tools/jEdit/src/jedit_main.scala \ src/Tools/jEdit/src/jedit_options.scala \ src/Tools/jEdit/src/jedit_plugins.scala \ src/Tools/jEdit/src/jedit_rendering.scala \ src/Tools/jEdit/src/jedit_resources.scala \ src/Tools/jEdit/src/jedit_sessions.scala \ src/Tools/jEdit/src/jedit_spell_checker.scala \ src/Tools/jEdit/src/keymap_merge.scala \ src/Tools/jEdit/src/main_plugin.scala \ src/Tools/jEdit/src/monitor_dockable.scala \ src/Tools/jEdit/src/output_dockable.scala \ src/Tools/jEdit/src/pide_docking_framework.scala \ src/Tools/jEdit/src/pretty_text_area.scala \ src/Tools/jEdit/src/pretty_tooltip.scala \ src/Tools/jEdit/src/process_indicator.scala \ src/Tools/jEdit/src/protocol_dockable.scala \ src/Tools/jEdit/src/query_dockable.scala \ src/Tools/jEdit/src/raw_output_dockable.scala \ src/Tools/jEdit/src/rich_text_area.scala \ src/Tools/jEdit/src/session_build.scala \ src/Tools/jEdit/src/simplifier_trace_dockable.scala \ src/Tools/jEdit/src/simplifier_trace_window.scala \ src/Tools/jEdit/src/sledgehammer_dockable.scala \ src/Tools/jEdit/src/state_dockable.scala \ src/Tools/jEdit/src/status_widget.scala \ src/Tools/jEdit/src/symbols_dockable.scala \ src/Tools/jEdit/src/syntax_style.scala \ src/Tools/jEdit/src/syslog_dockable.scala \ src/Tools/jEdit/src/text_overview.scala \ src/Tools/jEdit/src/text_structure.scala \ src/Tools/jEdit/src/theories_dockable.scala \ src/Tools/jEdit/src/timing_dockable.scala \ src/Tools/jEdit/src/token_markup.scala services = \ isabelle.Bash$Handler \ isabelle.Bibtex$File_Format \ isabelle.Document_Build$Build_Engine \ isabelle.Document_Build$LuaLaTeX_Engine \ isabelle.Document_Build$PDFLaTeX_Engine \ isabelle.ML_Statistics$Handler \ isabelle.Print_Operation$Handler \ isabelle.Scala$Handler \ isabelle.Scala_Functions \ isabelle.Server_Commands \ isabelle.Sessions$File_Format \ isabelle.Simplifier_Trace$Handler \ isabelle.Tools \ isabelle.jedit.JEdit_Plugin0 \ isabelle.jedit.JEdit_Plugin1 \ isabelle.nitpick.Kodkod$Handler \ isabelle.nitpick.Scala_Functions \ isabelle.spark.SPARK$Load_Command1 \ isabelle.spark.SPARK$Load_Command2 diff --git a/src/Pure/GUI/gui.scala b/src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala +++ b/src/Pure/GUI/gui.scala @@ -1,353 +1,353 @@ /* Title: Pure/GUI/gui.scala Author: Makarius Basic GUI tools (for AWT/Swing). */ package isabelle import java.util.{Map => JMap} import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point, Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit} import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute} import java.awt.geom.AffineTransform import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane, JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities} import scala.swing.{ComboBox, ScrollPane, TextArea} import scala.swing.event.SelectionChanged object GUI { /* Swing look-and-feel */ def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.setup() def current_laf: String = UIManager.getLookAndFeel.getClass.getName() def is_macos_laf: Boolean = Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf class Look_And_Feel(laf: LookAndFeel) extends Isabelle_System.Service { def info: UIManager.LookAndFeelInfo = new UIManager.LookAndFeelInfo(laf.getName, laf.getClass.getName) } lazy val look_and_feels: List[Look_And_Feel] = Isabelle_System.make_services(classOf[Look_And_Feel]) def init_lafs(): Unit = { val old_lafs = Set( "com.sun.java.swing.plaf.motif.MotifLookAndFeel", "com.sun.java.swing.plaf.windows.WindowsClassicLookAndFeel") val lafs = UIManager.getInstalledLookAndFeels().toList .filterNot(info => old_lafs(info.getClassName)) val more_lafs = look_and_feels.map(_.info) UIManager.setInstalledLookAndFeels((more_lafs ::: lafs).toArray) } /* additional look-and-feels */ /* plain focus traversal, notably for text fields */ def plain_focus_traversal(component: Component): Unit = { val dummy_button = new JButton def apply(id: Int): Unit = component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id)) apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS) apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS) } /* simple dialogs */ def scrollable_text( raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false ) : ScrollPane = { val txt = Output.clean_yxml(raw_txt) val text = new TextArea(txt) if (width > 0) text.columns = width if (height > 0 && split_lines(txt).length > height) text.rows = height text.editable = editable new ScrollPane(text) } private def simple_dialog( kind: Int, default_title: String, parent: Component, title: String, message: Iterable[Any] ): Unit = { GUI_Thread.now { val java_message = message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }). toArray.asInstanceOf[Array[AnyRef]] JOptionPane.showMessageDialog(parent, java_message, if (title == null) default_title else title, kind) } } def dialog(parent: Component, title: String, message: Any*): Unit = simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message) def warning_dialog(parent: Component, title: String, message: Any*): Unit = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message) def error_dialog(parent: Component, title: String, message: Any*): Unit = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message) def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int = GUI_Thread.now { val java_message = message map { case x: scala.swing.Component => x.peer case x => x } JOptionPane.showConfirmDialog(parent, java_message.toArray.asInstanceOf[Array[AnyRef]], title, option_type, JOptionPane.QUESTION_MESSAGE) } /* zoom box */ private val Zoom_Factor = "([0-9]+)%?".r abstract class Zoom_Box extends ComboBox[String]( List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%") ) { - def changed: Unit + def changed(): Unit def factor: Int = parse(selection.item) private def parse(text: String): Int = text match { case Zoom_Factor(s) => val i = Integer.parseInt(s) if (10 <= i && i < 1000) i else 100 case _ => 100 } private def print(i: Int): String = i.toString + "%" def set_item(i: Int): Unit = { peer.getEditor match { case null => case editor => editor.setItem(print(i)) } } makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x)) peer.getEditor.getEditorComponent match { case text: JTextField => text.setColumns(4) case _ => } selection.index = 3 listenTo(selection) - reactions += { case SelectionChanged(_) => changed } + reactions += { case SelectionChanged(_) => changed() } } /* tooltip with multi-line support */ def tooltip_lines(text: String): String = if (text == null || text == "") null else "" + HTML.output(text) + "" /* icon */ def isabelle_icon(): ImageIcon = new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle_transparent-32.gif")) def isabelle_icons(): List[ImageIcon] = for (icon <- List("isabelle/isabelle_transparent-32.gif", "isabelle/isabelle_transparent.gif")) yield new ImageIcon(getClass.getClassLoader.getResource(icon)) def isabelle_image(): Image = isabelle_icon().getImage /* location within multi-screen environment */ final case class Screen_Location(point: Point, bounds: Rectangle) { def relative(parent: Component, size: Dimension): Point = { val w = size.width val h = size.height val x0 = parent.getLocationOnScreen.x val y0 = parent.getLocationOnScreen.y val x1 = x0 + parent.getWidth - w val y1 = y0 + parent.getHeight - h val x2 = point.x min (bounds.x + bounds.width - w) val y2 = point.y min (bounds.y + bounds.height - h) val location = new Point((x2 min x1) max x0, (y2 min y1) max y0) SwingUtilities.convertPointFromScreen(location, parent) location } } def screen_location(component: Component, point: Point): Screen_Location = { val screen_point = new Point(point.x, point.y) if (component != null) SwingUtilities.convertPointToScreen(screen_point, component) val ge = GraphicsEnvironment.getLocalGraphicsEnvironment val screen_bounds = (for { device <- ge.getScreenDevices.iterator config <- device.getConfigurations.iterator bounds = config.getBounds } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds Screen_Location(screen_point, screen_bounds) } def mouse_location(): Screen_Location = screen_location(null, MouseInfo.getPointerInfo.getLocation) /* screen size */ sealed case class Screen_Size(bounds: Rectangle, insets: Insets) { def full_screen_bounds: Rectangle = if (Platform.is_linux) { // avoid menu bar and docking areas new Rectangle( bounds.x + insets.left, bounds.y + insets.top, bounds.width - insets.left - insets.right, bounds.height - insets.top - insets.bottom) } else if (Platform.is_macos) { // avoid menu bar, but ignore docking areas new Rectangle( bounds.x, bounds.y + insets.top, bounds.width, bounds.height - insets.top) } else bounds } def screen_size(component: Component): Screen_Size = { val config = component.getGraphicsConfiguration val bounds = config.getBounds val insets = Toolkit.getDefaultToolkit.getScreenInsets(config) Screen_Size(bounds, insets) } /* component hierachy */ def get_parent(component: Component): Option[Container] = component.getParent match { case null => None case parent => Some(parent) } def ancestors(component: Component): Iterator[Container] = new Iterator[Container] { private var next_elem = get_parent(component) def hasNext: Boolean = next_elem.isDefined def next(): Container = next_elem match { case Some(parent) => next_elem = get_parent(parent) parent case None => Iterator.empty.next() } } def parent_window(component: Component): Option[Window] = ancestors(component).collectFirst({ case x: Window => x }) def layered_pane(component: Component): Option[JLayeredPane] = parent_window(component) match { case Some(w: JWindow) => Some(w.getLayeredPane) case Some(w: JFrame) => Some(w.getLayeredPane) case Some(w: JDialog) => Some(w.getLayeredPane) case _ => None } def traverse_components(component: Component, apply: Component => Unit): Unit = { def traverse(comp: Component): Unit = { apply(comp) comp match { case cont: Container => for (i <- 0 until cont.getComponentCount) traverse(cont.getComponent(i)) case _ => } } traverse(component) } /* font operations */ def copy_font(font: Font): Font = if (font == null) null else new Font(font.getFamily, font.getStyle, font.getSize) def line_metrics(font: Font): LineMetrics = font.getLineMetrics("", new FontRenderContext(null, false, false)) def transform_font(font: Font, transform: AffineTransform): Font = font.deriveFont(JMap.of(TextAttribute.TRANSFORM, new TransformAttribute(transform))) def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font = new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) def label_font(): Font = (new JLabel).getFont /* Isabelle fonts */ def imitate_font( font: Font, family: String = Isabelle_Fonts.sans, scale: Double = 1.0 ): Font = { val font1 = new Font(family, font.getStyle, font.getSize) val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt) } def imitate_font_css( font: Font, family: String = Isabelle_Fonts.sans, scale: Double = 1.0 ): String = { val font1 = new Font(family, font.getStyle, font.getSize) val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;" } def use_isabelle_fonts(): Unit = { val default_font = label_font() val ui = UIManager.getDefaults for (prop <- List( "ToggleButton.font", "CheckBoxMenuItem.font", "Label.font", "Menu.font", "MenuItem.font", "PopupMenu.font", "Table.font", "TableHeader.font", "TextArea.font", "TextField.font", "TextPane.font", "ToolTip.font", "Tree.font")) { val font = ui.get(prop) match { case font: Font => font case _ => default_font } ui.put(prop, GUI.imitate_font(font)) } } } class FlatLightLaf extends GUI.Look_And_Feel(new com.formdev.flatlaf.FlatLightLaf) class FlatDarkLaf extends GUI.Look_And_Feel(new com.formdev.flatlaf.FlatDarkLaf) diff --git a/src/Pure/General/file.scala b/src/Pure/General/file.scala --- a/src/Pure/General/file.scala +++ b/src/Pure/General/file.scala @@ -1,336 +1,323 @@ /* Title: Pure/General/file.scala Author: Makarius File-system operations. */ package isabelle import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader, File => JFile, IOException} import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor, FileVisitOption, FileVisitResult} import java.nio.file.attribute.BasicFileAttributes import java.net.{URI, URL, MalformedURLException} import java.util.zip.{GZIPInputStream, GZIPOutputStream} import java.util.EnumSet import org.tukaani.xz.{XZInputStream, XZOutputStream} import scala.collection.mutable object File { /* standard path (Cygwin or Posix) */ def standard_path(path: Path): String = path.expand.implode def standard_path(platform_path: String): String = isabelle.setup.Environment.standard_path(platform_path) def standard_path(file: JFile): String = standard_path(file.getPath) def standard_url(name: String): String = try { val url = new URL(name) if (url.getProtocol == "file" && Url.is_wellformed_file(name)) standard_path(Url.parse_file(name)) else name } catch { case _: MalformedURLException => standard_path(name) } /* platform path (Windows or Posix) */ def platform_path(standard_path: String): String = isabelle.setup.Environment.platform_path(standard_path) def platform_path(path: Path): String = platform_path(standard_path(path)) def platform_file(path: Path): JFile = new JFile(platform_path(path)) /* platform files */ def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile def absolute_name(file: JFile): String = absolute(file).getPath def canonical(file: JFile): JFile = file.getCanonicalFile def canonical_name(file: JFile): String = canonical(file).getPath def path(file: JFile): Path = Path.explode(standard_path(file)) def pwd(): Path = path(Path.current.absolute_file) def uri(file: JFile): URI = file.toURI def uri(path: Path): URI = path.file.toURI def url(file: JFile): URL = uri(file).toURL def url(path: Path): URL = url(path.file) /* relative paths */ def relative_path(base: Path, other: Path): Option[Path] = { val base_path = base.java_path val other_path = other.java_path if (other_path.startsWith(base_path)) Some(path(base_path.relativize(other_path).toFile)) else None } /* bash path */ def bash_path(path: Path): String = Bash.string(standard_path(path)) def bash_path(file: JFile): String = Bash.string(standard_path(file)) def bash_platform_path(path: Path): String = Bash.string(platform_path(path)) /* directory entries */ def check_dir(path: Path): Path = if (path.is_dir) path else error("No such directory: " + path) def check_file(path: Path): Path = if (path.is_file) path else error("No such file: " + path) /* directory content */ def read_dir(dir: Path): List[String] = { if (!dir.is_dir) error("No such directory: " + dir.toString) val files = dir.file.listFiles if (files == null) Nil else files.toList.map(_.getName).sorted } def get_dir(dir: Path): String = read_dir(dir).filter(name => (dir + Path.basic(name)).is_dir) match { case List(entry) => entry case dirs => error("Exactly one directory entry expected: " + commas_quote(dirs.sorted)) } def find_files( start: JFile, pred: JFile => Boolean = _ => true, include_dirs: Boolean = false, follow_links: Boolean = false ): List[JFile] = { val result = new mutable.ListBuffer[JFile] def check(file: JFile): Unit = if (pred(file)) result += file if (start.isFile) check(start) else if (start.isDirectory) { val options = if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS) else EnumSet.noneOf(classOf[FileVisitOption]) Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE, new SimpleFileVisitor[JPath] { override def preVisitDirectory( path: JPath, attrs: BasicFileAttributes ): FileVisitResult = { if (include_dirs) check(path.toFile) FileVisitResult.CONTINUE } override def visitFile( path: JPath, attrs: BasicFileAttributes ): FileVisitResult = { val file = path.toFile if (include_dirs || !file.isDirectory) check(file) FileVisitResult.CONTINUE } } ) } result.toList } /* read */ def read(file: JFile): String = Bytes.read(file).text def read(path: Path): String = read(path.file) def read_stream(reader: BufferedReader): String = { val output = new StringBuilder(100) var c = -1 while ({ c = reader.read; c != -1 }) output += c.toChar reader.close() output.toString } def read_stream(stream: InputStream): String = read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) def read_gzip(file: JFile): String = read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_gzip(path: Path): String = read_gzip(path.file) def read_xz(file: JFile): String = read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_xz(path: Path): String = read_xz(path.file) /* read lines */ def read_line(reader: BufferedReader): Option[String] = { val line = try { reader.readLine} catch { case _: IOException => null } Option(line).map(Library.trim_line) } def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = { val result = new mutable.ListBuffer[String] var line: Option[String] = None while ({ line = read_line(reader); line.isDefined }) { progress(line.get) result += line.get } reader.close() result.toList } /* write */ def writer(file: JFile): BufferedWriter = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset)) def write_file( file: JFile, text: String, make_stream: OutputStream => OutputStream ): Unit = { val stream = make_stream(new FileOutputStream(file)) using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text)) } def write(file: JFile, text: String): Unit = write_file(file, text, s => s) def write(path: Path, text: String): Unit = write(path.file, text) def write_gzip(file: JFile, text: String): Unit = write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) def write_gzip(path: Path, text: String): Unit = write_gzip(path.file, text) def write_xz(file: JFile, text: String, options: XZ.Options): Unit = File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options)) def write_xz(file: JFile, text: String): Unit = write_xz(file, text, XZ.options()) def write_xz(path: Path, text: String, options: XZ.Options): Unit = write_xz(path.file, text, options) def write_xz(path: Path, text: String): Unit = write_xz(path, text, XZ.options()) def write_backup(path: Path, text: String): Unit = { if (path.is_file) Isabelle_System.move_file(path, path.backup) write(path, text) } def write_backup2(path: Path, text: String): Unit = { if (path.is_file) Isabelle_System.move_file(path, path.backup2) write(path, text) } /* append */ def append(file: JFile, text: String): Unit = Files.write(file.toPath, UTF8.bytes(text), StandardOpenOption.APPEND, StandardOpenOption.CREATE) def append(path: Path, text: String): Unit = append(path.file, text) /* change */ def change( path: Path, init: Boolean = false, strict: Boolean = false )(f: String => String): Unit = { if (!path.is_file && init) write(path, "") val x = read(path) val y = f(x) if (x != y) write(path, y) else if (strict) error("Unchanged file: " + path) } def change_lines(path: Path, init: Boolean = false, strict: Boolean = false)( f: List[String] => List[String]): Unit = change(path, init = init, strict = strict)(text => cat_lines(f(split_lines(text)))) /* eq */ def eq(file1: JFile, file2: JFile): Boolean = try { Files.isSameFile(file1.toPath, file2.toPath) } catch { case ERROR(_) => false } def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) /* eq_content */ def eq_content(file1: JFile, file2: JFile): Boolean = if (eq(file1, file2)) true else if (file1.length != file2.length) false else Bytes.read(file1) == Bytes.read(file2) def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file) /* permissions */ def is_executable(path: Path): Boolean = { if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok else path.file.canExecute } def set_executable(path: Path, flag: Boolean): Unit = { if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path) else if (Platform.is_windows) Isabelle_System.chmod("a-x", path) else path.file.setExecutable(flag, false) } /* content */ - object Content { - def apply(path: Path, content: Bytes): Content_Bytes = new Content_Bytes(path, content) - def apply(path: Path, content: String): Content_String = new Content_String(path, content) - def apply(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content) - } + def content(path: Path, content: Bytes): Content = new Content(path, content) + def content(path: Path, content: String): Content = new Content(path, Bytes(content)) + def content(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content) - trait Content { - def path: Path - def write(dir: Path): Unit + final class Content private[File](val path: Path, val content: Bytes) { override def toString: String = path.toString - } - final class Content_Bytes private[File](val path: Path, val content: Bytes) extends Content { def write(dir: Path): Unit = { val full_path = dir + path Isabelle_System.make_directory(full_path.expand.dir) Bytes.write(full_path, content) } } - final class Content_String private[File](val path: Path, val content: String) extends Content { - def write(dir: Path): Unit = { - val full_path = dir + path - Isabelle_System.make_directory(full_path.expand.dir) - File.write(full_path, content) - } - } + final class Content_XML private[File](val path: Path, val content: XML.Body) { + override def toString: String = path.toString - final class Content_XML private[File](val path: Path, val content: XML.Body) { - def output(out: XML.Body => String): Content_String = - new Content_String(path, out(content)) + def output(out: XML.Body => String): Content = new Content(path, Bytes(out(content))) } } diff --git a/src/Pure/General/mercurial.scala b/src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala +++ b/src/Pure/General/mercurial.scala @@ -1,618 +1,618 @@ /* Title: Pure/General/mercurial.scala Author: Makarius Support for Mercurial repositories, with local or remote repository clone and working directory (via ssh connection). */ package isabelle import scala.annotation.tailrec import scala.collection.mutable object Mercurial { type Graph = isabelle.Graph[String, Unit] /** HTTP server **/ object Server { def apply(root: String): Server = new Server(root) def start(root: Path): Server = { val hg = repository(root) val server_process = Future.promise[Bash.Process] val server_root = Future.promise[String] Isabelle_Thread.fork("hg") { val process = Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) } server_process.fulfill_result(process) Exn.release(process).result(progress_stdout = line => if (!server_root.is_finished) { server_root.fulfill(Library.try_unsuffix("/", line).getOrElse(line)) }) } server_process.join new Server(server_root.join) { override def close(): Unit = server_process.join.terminate() } } } class Server private(val root: String) extends AutoCloseable { override def toString: String = root def close(): Unit = () def changeset(rev: String = "tip", raw: Boolean = false): String = root + (if (raw) "/raw-rev/" else "/rev/") + rev def file(path: Path, rev: String = "tip", raw: Boolean = false): String = root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + path.expand.implode def archive(rev: String = "tip"): String = root + "/archive/" + rev + ".tar.gz" def read_changeset(rev: String = "tip"): String = Url.read(changeset(rev = rev, raw = true)) def read_file(path: Path, rev: String = "tip"): String = Url.read(file(path, rev = rev, raw = true)) def download_archive(rev: String = "tip", progress: Progress = new Progress): HTTP.Content = Isabelle_System.download(archive(rev = rev), progress = progress) def download_dir(dir: Path, rev: String = "tip", progress: Progress = new Progress): Unit = { Isabelle_System.new_directory(dir) Isabelle_System.with_tmp_file("rev", ext = ".tar.gz") { archive_path => val content = download_archive(rev = rev, progress = progress) Bytes.write(archive_path, content.bytes) progress.echo("Unpacking " + rev + ".tar.gz") Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path), dir = dir, original_owner = true, strip = 1).check } } } /** repository commands **/ /* command-line syntax */ def optional(s: String, prefix: String = ""): String = if (s == "") "" else " " + prefix + " " + Bash.string(s) def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else "" def opt_rev(s: String): String = optional(s, "--rev") def opt_template(s: String): String = optional(s, "--template") /* repository archives */ private val Archive_Node = """^node: (\S{12}).*$""".r private val Archive_Tag = """^tag: (\S+).*$""".r sealed case class Archive_Info(lines: List[String]) { def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a }) def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag } def archive_info(root: Path): Option[Archive_Info] = { val path = root + Path.explode(".hg_archival.txt") if (path.is_file) Some(Archive_Info(Library.trim_split_lines(File.read(path)))) else None } def archive_id(root: Path): Option[String] = archive_info(root).flatMap(_.id) def archive_tags(root: Path): Option[String] = archive_info(root).map(info => info.tags.mkString(" ")) /* hg_sync meta data */ object Hg_Sync { val NAME = ".hg_sync" val _NAME: String = " " + NAME val PATH: Path = Path.explode(NAME) val PATH_ID: Path = PATH + Path.explode("id") val PATH_LOG: Path = PATH + Path.explode("log") val PATH_DIFF: Path = PATH + Path.explode("diff") val PATH_STAT: Path = PATH + Path.explode("stat") def is_directory(root: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_dir(root + PATH) def directory(root: Path, ssh: SSH.System = SSH.Local): Directory = { if (is_directory(root, ssh = ssh)) new Directory(root, ssh) else error("No .hg_sync directory found in " + ssh.rsync_path(root)) } class Directory private [Hg_Sync](val root: Path, val ssh: SSH.System) { override def toString: String = ssh.rsync_path(root) def read(path: Path): String = ssh.read(root + path) lazy val id: String = read(PATH_ID) lazy val log: String = read(PATH_LOG) lazy val diff: String = read(PATH_DIFF) lazy val stat: String = read(PATH_STAT) def changed: Boolean = id.endsWith("+") } } /* repository access */ def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_dir(root + Path.explode(".hg")) && new Repository(root, ssh).command("root").ok def id_repository(root: Path, ssh: SSH.System = SSH.Local, rev: String = "tip"): Option[String] = if (is_repository(root, ssh = ssh)) Some(repository(root, ssh = ssh).id(rev = rev)) else None def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = { val hg = new Repository(root, ssh) hg.command("root").check hg } def self_repository(): Repository = repository(Path.ISABELLE_HOME) def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = { @tailrec def find(root: Path): Option[Repository] = if (is_repository(root, ssh)) Some(repository(root, ssh = ssh)) else if (root.is_root) None else find(root + Path.parent) find(ssh.expand_path(start)) } def the_repository(start: Path, ssh: SSH.System = SSH.Local): Repository = find_repository(start, ssh = ssh) getOrElse error("No repository found in " + start.absolute) private def make_repository( root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local ) : Repository = { val hg = new Repository(root, ssh) ssh.make_directory(hg.root.dir) hg.command(cmd, args, repository = false).check hg } def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository = make_repository(root, "init", ssh.bash_path(root), ssh = ssh) def clone_repository(source: String, root: Path, rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository = make_repository(root, "clone", options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh) def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository = { if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg } else clone_repository(source, root, options = "--noupdate", ssh = ssh) } class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local) { hg => val root: Path = ssh.expand_path(root_path) def root_url: String = ssh.hg_url + root.implode override def toString: String = ssh.hg_url + root.implode def command_line( name: String, args: String = "", options: String = "", repository: Boolean = true ): String = { "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + (if (repository) " --repository " + ssh.bash_path(root) else "") + " --noninteractive " + name + " " + options + " " + args } def command( name: String, args: String = "", options: String = "", repository: Boolean = true ): Process_Result = { ssh.execute(command_line(name, args = args, options = options, repository = repository)) } def add(files: List[Path]): Unit = hg.command("add", files.map(ssh.bash_path).mkString(" ")) def archive(target: String, rev: String = "", options: String = ""): Unit = hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check def heads(template: String = "{node|short}\n", options: String = ""): List[String] = hg.command("heads", opt_template(template), options).check.out_lines def identify(rev: String = "tip", options: String = ""): String = hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse "" def id(rev: String = "tip"): String = identify(rev, options = "-i") def tags(rev: String = "tip"): String = { val result = identify(rev, options = "-t") Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ") } def paths(args: String = "", options: String = ""): List[String] = hg.command("paths", args = args, options = options).check.out_lines def manifest(rev: String = "", options: String = ""): List[String] = hg.command("manifest", opt_rev(rev), options).check.out_lines def log(rev: String = "", template: String = "", options: String = ""): String = hg.command("log", opt_rev(rev) + opt_template(template), options).check.out def diff(rev: String = "", options: String = ""): String = hg.command("diff", opt_rev(rev), options).check.out def parent(): String = log(rev = "p1()", template = "{node|short}") def push( remote: String = "", rev: String = "", force: Boolean = false, options: String = "" ): Unit = { hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options). check_rc(rc => rc == 0 | rc == 1) } def pull(remote: String = "", rev: String = "", options: String = ""): Unit = hg.command("pull", opt_rev(rev) + optional(remote), options).check def update( rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "" ): Unit = { hg.command("update", opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check } def status(options: String = ""): List[String] = hg.command("status", options = options).check.out_lines def known_files(): List[String] = status(options = "--modified --added --clean --no-status") def sync(context: Rsync.Context, target: String, verbose: Boolean = false, thorough: Boolean = false, dry_run: Boolean = false, filter: List[String] = Nil, contents: List[File.Content] = Nil, rev: String = "" ): Unit = { require(ssh == SSH.Local, "local repository required") Isabelle_System.with_tmp_dir("sync") { tmp_dir => val context0 = context.copy(progress = new Progress) Rsync.init(context0, target) val list = Rsync.exec(context0, list = true, args = List("--", Rsync.terminate(target))) .check.out_lines.filterNot(_.endsWith(" .")) if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) { error("No .hg_sync meta data in " + quote(target)) } val id_content = id(rev = rev) val is_changed = id_content.endsWith("+") val log_content = if (is_changed) "" else log(rev = rev, options = "-l1") val diff_content = if (is_changed) diff(rev = rev, options = "--git") else "" val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else "" Rsync.init(context0, target, contents = - File.Content(Hg_Sync.PATH_ID, id_content) :: - File.Content(Hg_Sync.PATH_LOG, log_content) :: - File.Content(Hg_Sync.PATH_DIFF, diff_content) :: - File.Content(Hg_Sync.PATH_STAT, stat_content) :: contents) + File.content(Hg_Sync.PATH_ID, id_content) :: + File.content(Hg_Sync.PATH_LOG, log_content) :: + File.content(Hg_Sync.PATH_DIFF, diff_content) :: + File.content(Hg_Sync.PATH_STAT, stat_content) :: contents) val (exclude, source) = if (rev.isEmpty) { val exclude = ".hg" :: status(options = "--unknown --ignored --no-status") val source = File.standard_path(root) (exclude, source) } else { val exclude = List(".hg_archival.txt") val source = File.standard_path(tmp_dir + Path.explode("archive")) archive(source, rev = rev) (exclude, source) } val exclude_path = tmp_dir + Path.explode("exclude") File.write(exclude_path, cat_lines(exclude.map("/" + _))) val protect = (Hg_Sync.PATH :: contents.map(_.path)) .map(path => "protect /" + File.standard_path(path)) Rsync.exec(context, verbose = verbose, thorough = thorough, dry_run = dry_run, clean = true, prune_empty_dirs = true, filter = protect ::: filter, args = List("--exclude-from=" + exclude_path.implode, "--", Rsync.terminate(source), target) ).check } } def graph(): Graph = { val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r val log_result = log(template = """node: {node|short} {p1node|short} {p2node|short}\n""") split_lines(log_result).foldLeft(Graph.string[Unit]) { case (graph, Node(x, y, z)) => val deps = List(y, z).filterNot(s => s.forall(_ == '0')) val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ())) deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) }) case (graph, _) => graph } } } /** check files **/ def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) = { val outside = new mutable.ListBuffer[Path] val unknown = new mutable.ListBuffer[Path] @tailrec def check(paths: List[Path]): Unit = { paths match { case path :: rest => find_repository(path, ssh) match { case None => outside += path; check(rest) case Some(hg) => val known = hg.known_files().iterator.map(name => (hg.root + Path.explode(name)).canonical_file).toSet if (!known(path.canonical_file)) unknown += path check(rest.filterNot(p => known(p.canonical_file))) } case Nil => } } check(files) (outside.toList, unknown.toList) } /** hg_setup **/ private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit = { val hgrc = local_hg.root + Path.explode(".hg/hgrc") def header(line: String): Boolean = line.startsWith("[paths]") val Entry = """^(\S+)\s*=\s*(.*)$""".r val new_entry = path_name + " = " + source def commit(lines: List[String]): Boolean = { File.write(hgrc, cat_lines(lines)) true } val edited = hgrc.is_file && { val lines = split_lines(File.read(hgrc)) lines.count(header) == 1 && { if (local_hg.paths(options = "-q").contains(path_name)) { val old_source = local_hg.paths(args = path_name).head val old_entry = path_name + ".old = " + old_source val lines1 = lines.map { case Entry(a, b) if a == path_name && b == old_source => new_entry + "\n" + old_entry case line => line } lines != lines1 && commit(lines1) } else { val prefix = lines.takeWhile(line => !header(line)) val n = prefix.length commit(prefix ::: List(lines(n), new_entry) ::: lines.drop(n + 1)) } } } if (!edited) File.append(hgrc, "\n[paths]\n" + new_entry + "\n") } val default_path_name = "default" def hg_setup( remote: String, local_path: Path, remote_name: String = "", path_name: String = default_path_name, remote_exists: Boolean = false, progress: Progress = new Progress ): Unit = { /* local repository */ Isabelle_System.make_directory(local_path) val repos_name = proper_string(remote_name) getOrElse local_path.absolute.base.implode val local_hg = if (is_repository(local_path)) repository(local_path) else init_repository(local_path) progress.echo("Local repository " + local_hg.root.absolute) /* remote repository */ val remote_url = remote match { case _ if remote.startsWith("ssh://") => val ssh_url = remote + "/" + repos_name if (!remote_exists) { try { local_hg.command("init", ssh_url, repository = false).check } catch { case ERROR(msg) => progress.echo_warning(msg) } } ssh_url case SSH.Target(user, host) => val phabricator = Phabricator.API(user, host) var repos = phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse { if (remote_exists) { error("Remote repository " + quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist") } else phabricator.create_repository(repos_name, short_name = repos_name) } while (repos.importing) { progress.echo("Awaiting remote repository ...") Time.seconds(0.5).sleep() repos = phabricator.the_repository(repos.phid) } repos.ssh_url case _ => error("Malformed remote specification " + quote(remote)) } progress.echo("Remote repository " + quote(remote_url)) /* synchronize local and remote state */ progress.echo("Synchronizing ...") edit_hgrc(local_hg, path_name, remote_url) local_hg.pull(options = "-u") local_hg.push(remote = remote_url) } val isabelle_tool1 = Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository", Scala_Project.here, { args => var remote_name = "" var path_name = default_path_name var remote_exists = false val getopts = Getopts(""" Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR Options are: -n NAME remote repository name (default: base name of LOCAL_DIR) -p PATH Mercurial path name (default: """ + quote(default_path_name) + """) -r assume that remote repository already exists Setup a remote vs. local Mercurial repository: REMOTE either refers to a Phabricator server "user@host" or SSH file server "ssh://user@host/path". """, "n:" -> (arg => remote_name = arg), "p:" -> (arg => path_name = arg), "r" -> (_ => remote_exists = true)) val more_args = getopts(args) val (remote, local_path) = more_args match { case List(arg1, arg2) => (arg1, Path.explode(arg2)) case _ => getopts.usage() } val progress = new Console_Progress hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name, remote_exists = remote_exists, progress = progress) }) /** hg_sync **/ val isabelle_tool2 = Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory", Scala_Project.here, { args => var filter: List[String] = Nil var root: Option[Path] = None var protect_args = false var thorough = false var dry_run = false var rev = "" var port = SSH.default_port var verbose = false val getopts = Getopts(""" Usage: isabelle hg_sync [OPTIONS] TARGET Options are: -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion) -R ROOT explicit repository root directory (default: implicit from current directory) -S robust (but less portable) treatment of spaces in file and directory names on the target -T thorough treatment of file content and directory times -n no changes: dry-run -r REV explicit revision (default: state of working directory) -p PORT explicit SSH port (default: """ + SSH.default_port + """) -v verbose Synchronize Mercurial repository with TARGET directory, which can be local or remote (using notation of rsync). """, "F:" -> (arg => filter = filter ::: List(arg)), "R:" -> (arg => root = Some(Path.explode(arg))), "S" -> (_ => protect_args = true), "T" -> (_ => thorough = true), "n" -> (_ => dry_run = true), "r:" -> (arg => rev = arg), "p:" -> (arg => port = Value.Int.parse(arg)), "v" -> (_ => verbose = true)) val more_args = getopts(args) val target = more_args match { case List(target) => target case _ => getopts.usage() } val progress = new Console_Progress val hg = root match { case Some(dir) => repository(dir) case None => the_repository(Path.current) } val context = Rsync.Context(progress, port = port, protect_args = protect_args) hg.sync(context, target, verbose = verbose, thorough = thorough, dry_run = dry_run, filter = filter, rev = rev) } ) } 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,1239 +1,1218 @@ /* 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): 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 = command.span.content.foldLeft(p)(_.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 + case None => command_iterator().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(del.foldLeft(graph)(_.del_node(_)))) } def + (entry: (Node.Name, Node)): Nodes = { val (name, node) = entry val imports = node.header.imports val graph1 = imports.foldLeft(graph.default_node(name, Node.empty)) { case (g, p) => g.default_node(p, Node.empty) } val graph2 = graph1.imm_preds(name).foldLeft(graph1) { case (g, dep) => g.del_edge(dep, name) } val graph3 = imports.foldLeft(graph2) { case (g, dep) => g.add_edge(dep, name) } new Nodes(graph3.map_node(name, _ => node)) } 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] = { (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)). foldLeft(versions)(_ + _) } } 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 = edits.foldLeft(offset) { case (i, edit) => edit.convert(i) } def revert(offset: Text.Offset): Text.Offset = reverse_edits.foldLeft(offset) { case (i, edit) => edit.revert(i) } def convert(range: Text.Range): Text.Range = range.map(convert) def revert(range: Text.Range): Text.Range = range.map(revert) /* 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 all_exports: Map[Export.Entry_Name, Export.Entry] = (for { (name, _) <- version.nodes.iterator (_, entry) <- state.node_exports(version, name).iterator if entry.entry_name.session == Sessions.DRAFT } yield entry.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 = sources_iterator.foldLeft(Line.Position.zero)(_.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 => _ => 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, "assignment not finished"); this } def unfinished: Assignment = new Assignment(command_execs, false) def assign(update: Assign_Update): Assignment = { require(!is_finished, "assignment already finished") val command_execs1 = update.foldLeft(command_execs) { 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] = st.markups.redirection_iterator.foldLeft(commands_redirection) { case (graph, id) => graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) } def accumulate( id: Document_ID.Generic, message: XML.Elem, cache: XML.Cache ) : (Command.State, State) = { 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) = update.foldLeft((List.empty[Command], execs)) { 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), "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), "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), "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 = rev_pending_changes.foldLeft(pending_edits) { case (edits, Node.Edits(es)) => es ::: edits case (edits, _) => edits } new Snapshot(this, version, node_name, edits, snippet_command) } def snippet(command: Command): Snapshot = snapshot().snippet(command) } } diff --git a/src/Pure/System/classpath.scala b/src/Pure/System/classpath.scala --- a/src/Pure/System/classpath.scala +++ b/src/Pure/System/classpath.scala @@ -1,95 +1,95 @@ /* Title: Pure/System/classpath.scala Author: Makarius Java classpath and Scala services. */ package isabelle import java.io.{File => JFile} import java.nio.file.Files import java.net.URLClassLoader import scala.jdk.CollectionConverters._ object Classpath { abstract class Service type Service_Class = Class[Service] def apply( jar_files: List[JFile] = Nil, - jar_contents: List[File.Content_Bytes] = Nil): Classpath = + jar_contents: List[File.Content] = Nil): Classpath = { val jar_files0 = for { s <- space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", "")) if s.nonEmpty } yield File.absolute(new JFile(s)) val jar_files1 = jar_files.flatMap(start => File.find_files(start, _.getName.endsWith(".jar"))) .map(File.absolute) val tmp_jars = for (jar <- jar_contents) yield { val tmp_jar = Files.createTempFile("jar", "jar").toFile tmp_jar.deleteOnExit() Bytes.write(tmp_jar, jar.content) tmp_jar } new Classpath(jar_files0 ::: jar_files1, tmp_jars) } } class Classpath private(static_jars: List[JFile], dynamic_jars: List[JFile]) { def jars: List[JFile] = static_jars ::: dynamic_jars override def toString: String = jars.mkString("Classpath(", ", ", ")") def platform_path: String = jars.map(_.getPath).mkString(JFile.pathSeparator) val class_loader: ClassLoader = { val this_class_loader = this.getClass.getClassLoader if (dynamic_jars.isEmpty) this_class_loader else { new URLClassLoader(dynamic_jars.map(File.url).toArray, this_class_loader) { override def finalize(): Unit = { for (jar <- dynamic_jars) { try { jar.delete() } catch { case _: Throwable => } } } } } } private def init_services(where: String, names: List[String]): List[Classpath.Service_Class] = { for (name <- names) yield { def err(msg: String): Nothing = error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg) try { Class.forName(name, true, class_loader).asInstanceOf[Classpath.Service_Class] } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } } val services: List[Classpath.Service_Class] = { val variable = "ISABELLE_SCALA_SERVICES" val services_env = init_services(quote(variable), space_explode(':', Isabelle_System.getenv_strict(variable))) val services_jars = jars.flatMap(jar => init_services(File.standard_path(jar), isabelle.setup.Build.get_services(jar.toPath).asScala.toList)) services_env ::: services_jars } def make_services[C](c: Class[C]): List[C] = for { c1 <- services if Library.is_subclass(c1, c) } yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C] } diff --git a/src/Pure/Thy/document_build.scala b/src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala +++ b/src/Pure/Thy/document_build.scala @@ -1,490 +1,509 @@ /* Title: Pure/Thy/document_build.scala Author: Makarius Build theory document (PDF) from session database. */ package isabelle object Document_Build { /* document variants */ abstract class Document_Name { def name: String def path: Path = Path.basic(name) override def toString: String = name } object Document_Variant { def parse(opt: String): Document_Variant = Library.space_explode('=', opt) match { case List(name) => Document_Variant(name, Latex.Tags.empty) case List(name, tags) => Document_Variant(name, Latex.Tags(tags)) case _ => error("Malformed document variant: " + quote(opt)) } } sealed case class Document_Variant(name: String, tags: Latex.Tags) extends Document_Name { def print: String = if (tags.toString.isEmpty) name else name + "=" + tags.toString } sealed case class Document_Input(name: String, sources: SHA1.Digest) - extends Document_Name + extends Document_Name { override def toString: String = name } sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes) extends Document_Name { + override def toString: String = name + def log: String = log_xz.uncompress().text def log_lines: List[String] = split_lines(log) def write(db: SQL.Database, session_name: String): Unit = write_document(db, session_name, this) def write(dir: Path): Path = { val path = dir + Path.basic(name).pdf Isabelle_System.make_directory(path.expand.dir) Bytes.write(path, pdf) path } } /* SQL data model */ object Data { val session_name = SQL.Column.string("session_name").make_primary_key val name = SQL.Column.string("name").make_primary_key val sources = SQL.Column.string("sources") val log_xz = SQL.Column.bytes("log_xz") val pdf = SQL.Column.bytes("pdf") val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf)) def where_equal(session_name: String, name: String = ""): SQL.Source = "WHERE " + Data.session_name.equal(session_name) + (if (name == "") "" else " AND " + Data.name.equal(name)) } def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = { val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name)) db.using_statement(select)(stmt => stmt.execute_query().iterator({ res => val name = res.string(Data.name) val sources = res.string(Data.sources) Document_Input(name, SHA1.fake_digest(sources)) }).toList) } def read_document( db: SQL.Database, session_name: String, name: String ): Option[Document_Output] = { val select = Data.table.select(sql = Data.where_equal(session_name, name)) db.using_statement(select)({ stmt => val res = stmt.execute_query() if (res.next()) { val name = res.string(Data.name) val sources = res.string(Data.sources) val log_xz = res.bytes(Data.log_xz) val pdf = res.bytes(Data.pdf) Some(Document_Output(name, SHA1.fake_digest(sources), log_xz, pdf)) } else None }) } def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = { db.using_statement(Data.table.insert()){ stmt => stmt.string(1) = session_name stmt.string(2) = doc.name stmt.string(3) = doc.sources.toString stmt.bytes(4) = doc.log_xz stmt.bytes(5) = doc.pdf stmt.execute() } } /* context */ val texinputs: Path = Path.explode("~~/lib/texinputs") val isabelle_styles: List[Path] = List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty"). map(name => texinputs + Path.basic(name)) def context( session_context: Export.Session_Context, + document_session: Option[Sessions.Base] = None, progress: Progress = new Progress - ): Context = new Context(session_context, progress) + ): Context = new Context(session_context, document_session, progress) final class Context private[Document_Build]( - val session_context: Export.Session_Context, + session_context: Export.Session_Context, + document_session: Option[Sessions.Base], val progress: Progress = new Progress ) { + context => + + /* session info */ - def session: String = session_context.session_name + private val base = document_session getOrElse session_context.session_base + private val info = session_context.sessions_structure(base.session_name) - private val info = session_context.sessions_structure(session) - private val base = session_context.session_base + def session: String = info.name + def options: Options = info.options - val classpath: List[File.Content_Bytes] = session_context.classpath() + override def toString: String = session - def options: Options = info.options + val classpath: List[File.Content] = session_context.classpath() def document_bibliography: Boolean = options.bool("document_bibliography") def document_logo: Option[String] = options.string("document_logo") match { case "" => None case "_" => Some("") case name => Some(name) } def document_build: String = options.string("document_build") def get_engine(): Engine = { val name = document_build Classpath(jar_contents = classpath).make_services(classOf[Engine]) .find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name))) } /* document content */ def documents: List[Document_Variant] = info.documents def proper_session_theories: List[Document.Node.Name] = base.proper_session_theories def document_theories: List[Document.Node.Name] = proper_session_theories ::: base.document_theories lazy val document_latex: List[File.Content_XML] = for (name <- document_theories) yield { val path = Path.basic(tex_name(name)) val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true) val content = YXML.parse_body(entry.text) - File.Content(path, content) + File.content(path, content) } lazy val session_graph: File.Content = { val path = Presentation.session_graph_path val content = graphview.Graph_File.make_pdf(options, base.session_graph_display) - File.Content(path, content) + File.content(path, content) } lazy val session_tex: File.Content = { val path = Path.basic("session.tex") val content = Library.terminate_lines( base.proper_session_theories.map(name => "\\input{" + tex_name(name) + "}")) - File.Content(path, content) + File.content(path, content) } lazy val isabelle_logo: Option[File.Content] = { document_logo.map(logo_name => Isabelle_System.with_tmp_file("logo", ext = "pdf") { tmp_path => Logo.create_logo(logo_name, output_file = tmp_path, quiet = true) val path = Path.basic("isabelle_logo.pdf") val content = Bytes.read(tmp_path) - File.Content(path, content) + File.content(path, content) }) } + /* build document */ + + def build_document(doc: Document_Variant, verbose: Boolean = false): Document_Output = { + Isabelle_System.with_tmp_dir("document") { tmp_dir => + val engine = get_engine() + val directory = engine.prepare_directory(context, tmp_dir, doc) + engine.build_document(context, directory, verbose) + } + } + + /* document directory */ def prepare_directory( dir: Path, doc: Document_Variant, latex_output: Latex.Output ): Directory = { val doc_dir = Isabelle_System.make_directory(dir + Path.basic(doc.name)) /* actual sources: with SHA1 digest */ isabelle_styles.foreach(Isabelle_System.copy_file(_, doc_dir)) val comment_latex = options.bool("document_comment_latex") if (!comment_latex) { Isabelle_System.copy_file(texinputs + Path.basic("comment.sty"), doc_dir) } doc.tags.sty(comment_latex).write(doc_dir) for ((base_dir, src) <- info.document_files) { Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir) } session_tex.write(doc_dir) for (content <- document_latex) { content.output(latex_output(_, file_pos = content.path.implode_symbolic)) .write(doc_dir) } val root_name1 = "root_" + doc.name val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root" val digests1 = List(doc.print, document_logo.toString, document_build).map(SHA1.digest) val digests2 = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest) val sources = SHA1.digest_set(digests1 ::: digests2) /* derived material: without SHA1 digest */ isabelle_logo.foreach(_.write(doc_dir)) session_graph.write(doc_dir) Directory(doc_dir, doc, root_name, sources) } def old_document(directory: Directory): Option[Document_Output] = for { db <- session_context.session_db() old_doc <- read_document(db, session, directory.doc.name) if old_doc.sources == directory.sources } yield old_doc } sealed case class Directory( doc_dir: Path, doc: Document_Variant, root_name: String, sources: SHA1.Digest ) { def root_name_script(ext: String = ""): String = Bash.string(if (ext.isEmpty) root_name else root_name + "." + ext) def conditional_script(ext: String, exe: String, after: String = ""): String = "if [ -f " + root_name_script(ext) + " ]\n" + "then\n" + " " + exe + " " + root_name_script() + "\n" + (if (after.isEmpty) "" else " " + after) + "fi\n" def log_errors(): List[String] = Latex.latex_errors(doc_dir, root_name) ::: Bibtex.bibtex_errors(doc_dir, root_name) def make_document(log: List[String], errors: List[String]): Document_Output = { val root_pdf = Path.basic(root_name).pdf val result_pdf = doc_dir + root_pdf if (errors.nonEmpty) { val errors1 = errors ::: List("Failed to build document " + quote(doc.name)) throw new Build_Error(log, Exn.cat_message(errors1: _*)) } else if (!result_pdf.is_file) { val message = "Bad document result: expected to find " + root_pdf throw new Build_Error(log, message) } else { val log_xz = Bytes(cat_lines(log)).compress() val pdf = Bytes.read(result_pdf) Document_Output(doc.name, sources, log_xz, pdf) } } } /* build engines */ abstract class Engine(val name: String) extends Isabelle_System.Service { override def toString: String = name def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory def build_document(context: Context, directory: Directory, verbose: Boolean): Document_Output } abstract class Bash_Engine(name: String) extends Engine(name) { def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory = context.prepare_directory(dir, doc, new Latex.Output(context.options)) def use_pdflatex: Boolean = false def latex_script(context: Context, directory: Directory): String = (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") + " " + directory.root_name_script() + "\n" def bibtex_script(context: Context, directory: Directory, latex: Boolean = false): String = { val ext = if (context.document_bibliography) "aux" else "bib" directory.conditional_script(ext, "$ISABELLE_BIBTEX", after = if (latex) latex_script(context, directory) else "") } def makeindex_script(context: Context, directory: Directory, latex: Boolean = false): String = directory.conditional_script("idx", "$ISABELLE_MAKEINDEX", after = if (latex) latex_script(context, directory) else "") def use_build_script: Boolean = false def build_script(context: Context, directory: Directory): String = { val has_build_script = (directory.doc_dir + Path.explode("build")).is_file if (!use_build_script && has_build_script) { error("Unexpected document build script for option document_build=" + quote(context.document_build)) } else if (use_build_script && !has_build_script) error("Missing document build script") else if (has_build_script) "./build pdf " + Bash.string(directory.doc.name) else { "set -e\n" + latex_script(context, directory) + bibtex_script(context, directory, latex = true) + makeindex_script(context, directory) + latex_script(context, directory) + makeindex_script(context, directory, latex = true) } } def build_document( context: Context, directory: Directory, verbose: Boolean ): Document_Output = { val result = context.progress.bash( build_script(context, directory), cwd = directory.doc_dir.file, echo = verbose, watchdog = Time.seconds(0.5)) val log = result.out_lines ::: result.err_lines val errors = (if (result.ok) Nil else List(result.err)) ::: directory.log_errors() directory.make_document(log, errors) } } class LuaLaTeX_Engine extends Bash_Engine("lualatex") class PDFLaTeX_Engine extends Bash_Engine("pdflatex") { override def use_pdflatex: Boolean = true } class Build_Engine extends Bash_Engine("build") { override def use_build_script: Boolean = true } /* build documents */ def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex" class Build_Error(val log_lines: List[String], val message: String) extends Exn.User_Error(message) def build_documents( context: Context, output_sources: Option[Path] = None, output_pdf: Option[Path] = None, verbose: Boolean = false ): List[Document_Output] = { val progress = context.progress val engine = context.get_engine() val documents = for (doc <- context.documents) yield { Isabelle_System.with_tmp_dir("document") { tmp_dir => progress.echo("Preparing " + context.session + "/" + doc.name + " ...") val start = Time.now() output_sources.foreach(engine.prepare_directory(context, _, doc)) val directory = engine.prepare_directory(context, tmp_dir, doc) val document = context.old_document(directory) getOrElse engine.build_document(context, directory, verbose) val stop = Time.now() val timing = stop - start progress.echo("Finished " + context.session + "/" + doc.name + " (" + timing.message_hms + " elapsed time)") document } } for (dir <- output_pdf; doc <- documents) { val path = doc.write(dir) progress.echo("Document at " + path.absolute) } documents } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, { args => var output_sources: Option[Path] = None var output_pdf: Option[Path] = None var verbose_latex = false var dirs: List[Path] = Nil var options = Options.init() var verbose_build = false val getopts = Getopts(""" Usage: isabelle document [OPTIONS] SESSION Options are: -O DIR output directory for LaTeX sources and resulting PDF -P DIR output directory for resulting PDF -S DIR output directory for LaTeX sources -V verbose latex -d DIR include session directory -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose build Prepare the theory document of a session. """, "O:" -> (arg => { val dir = Path.explode(arg) output_sources = Some(dir) output_pdf = Some(dir) }), "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }), "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }), "V" -> (_ => verbose_latex = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose_build = true)) val more_args = getopts(args) val session = more_args match { case List(a) => a case _ => getopts.usage() } val progress = new Console_Progress(verbose = verbose_build) val store = Sessions.store(options) progress.interrupt_handler { val res = Build.build(options, selection = Sessions.Selection.session(session), dirs = dirs, progress = progress, verbose = verbose_build) if (!res.ok) error("Failed to build session " + quote(session)) val deps = Sessions.load_structure(options + "document=pdf", dirs = dirs). selection_deps(Sessions.Selection.session(session)) val session_base_info = deps.base_info(session) if (output_sources.isEmpty && output_pdf.isEmpty) { progress.echo_warning("No output directory") } using(Export.open_session_context(store, session_base_info)) { session_context => build_documents( context(session_context, progress = progress), output_sources = output_sources, output_pdf = output_pdf, verbose = verbose_latex) } } }) } diff --git a/src/Pure/Thy/export.scala b/src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala +++ b/src/Pure/Thy/export.scala @@ -1,572 +1,572 @@ /* Title: Pure/Thy/export.scala Author: Makarius Manage theory exports: compressed blobs. */ package isabelle import scala.annotation.tailrec import scala.util.matching.Regex object Export { /* artefact names */ val DOCUMENT_ID = "PIDE/document_id" val FILES = "PIDE/files" val MARKUP = "PIDE/markup" val MESSAGES = "PIDE/messages" val DOCUMENT_PREFIX = "document/" val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex" val DOCUMENT_CITATIONS = DOCUMENT_PREFIX + "citations" val THEORY_PREFIX: String = "theory/" val PROOFS_PREFIX: String = "proofs/" val THEORY_PARENTS: String = THEORY_PREFIX + "parents" def explode_name(s: String): List[String] = space_explode('/', s) def implode_name(elems: Iterable[String]): String = elems.mkString("/") /* SQL data model */ object Data { val session_name = SQL.Column.string("session_name").make_primary_key val theory_name = SQL.Column.string("theory_name").make_primary_key val name = SQL.Column.string("name").make_primary_key val executable = SQL.Column.bool("executable") val compressed = SQL.Column.bool("compressed") val body = SQL.Column.bytes("body") val table = SQL.Table("isabelle_exports", List(session_name, theory_name, name, executable, compressed, body)) def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source = "WHERE " + Data.session_name.equal(session_name) + (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) + (if (name == "") "" else " AND " + Data.name.equal(name)) } def compound_name(a: String, b: String): String = if (a.isEmpty) b else a + ":" + b sealed case class Entry_Name(session: String = "", theory: String = "", name: String = "") { val compound_name: String = Export.compound_name(theory, name) def make_path(prune: Int = 0): Path = { val elems = theory :: space_explode('/', name) if (elems.length < prune + 1) { error("Cannot prune path by " + prune + " element(s): " + Path.make(elems)) } else Path.make(elems.drop(prune)) } def readable(db: SQL.Database): Boolean = { val select = Data.table.select(List(Data.name), Data.where_equal(session, theory, name)) db.using_statement(select)(stmt => stmt.execute_query().next()) } def read(db: SQL.Database, cache: XML.Cache): Option[Entry] = { val select = Data.table.select(List(Data.executable, Data.compressed, Data.body), Data.where_equal(session, theory, name)) db.using_statement(select) { stmt => val res = stmt.execute_query() if (res.next()) { val executable = res.bool(Data.executable) val compressed = res.bool(Data.compressed) val bytes = res.bytes(Data.body) val body = Future.value(compressed, bytes) Some(Entry(this, executable, body, cache)) } else None } } } def read_theory_names(db: SQL.Database, session_name: String): List[String] = { val select = Data.table.select(List(Data.theory_name), Data.where_equal(session_name, name = THEORY_PARENTS)) + " ORDER BY " + Data.theory_name db.using_statement(select)(stmt => stmt.execute_query().iterator(_.string(Data.theory_name)).toList) } def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] = { val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) + " ORDER BY " + Data.theory_name + ", " + Data.name db.using_statement(select)(stmt => stmt.execute_query().iterator(res => Entry_Name(session = session_name, theory = res.string(Data.theory_name), name = res.string(Data.name))).toList) } def message(msg: String, theory_name: String, name: String): String = msg + " " + quote(name) + " for theory " + quote(theory_name) def empty_entry(theory_name: String, name: String): Entry = Entry(Entry_Name(theory = theory_name, name = name), false, Future.value(false, Bytes.empty), XML.Cache.none) sealed case class Entry( entry_name: Entry_Name, executable: Boolean, body: Future[(Boolean, Bytes)], cache: XML.Cache ) { def session_name: String = entry_name.session def theory_name: String = entry_name.theory def name: String = entry_name.name override def toString: String = name def compound_name: String = entry_name.compound_name def name_has_prefix(s: String): Boolean = name.startsWith(s) val name_elems: List[String] = explode_name(name) def name_extends(elems: List[String]): Boolean = name_elems.startsWith(elems) && name_elems != elems def text: String = uncompressed.text def uncompressed: Bytes = { val (compressed, bytes) = body.join if (compressed) bytes.uncompress(cache = cache.xz) else bytes } def uncompressed_yxml: XML.Body = YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache) def write(db: SQL.Database): Unit = { val (compressed, bytes) = body.join db.using_statement(Data.table.insert()) { stmt => stmt.string(1) = session_name stmt.string(2) = theory_name stmt.string(3) = name stmt.bool(4) = executable stmt.bool(5) = compressed stmt.bytes(6) = bytes stmt.execute() } } } def make_regex(pattern: String): Regex = { @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = chs match { case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) case '*' :: rest => make("[^:/]*" :: result, depth, rest) case '?' :: rest => make("[^:/]" :: result, depth, rest) case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) case '{' :: rest => make("(" :: result, depth + 1, rest) case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest) case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest) case c :: rest => make(c.toString :: result, depth, rest) case Nil => result.reverse.mkString.r } make(Nil, 0, pattern.toList) } def make_matcher(pats: List[String]): Entry_Name => Boolean = { val regs = pats.map(make_regex) (entry_name: Entry_Name) => regs.exists(_.pattern.matcher(entry_name.compound_name).matches) } def make_entry( session_name: String, args: Protocol.Export.Args, bytes: Bytes, cache: XML.Cache ): Entry = { val body = if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz)) else Future.value((false, bytes)) val entry_name = Entry_Name(session = session_name, theory = args.theory_name, name = args.name) Entry(entry_name, args.executable, body, cache) } /* database consumer thread */ def consumer(db: SQL.Database, cache: XML.Cache, progress: Progress = new Progress): Consumer = new Consumer(db, cache, progress) class Consumer private[Export](db: SQL.Database, cache: XML.Cache, progress: Progress) { private val errors = Synchronized[List[String]](Nil) private val consumer = Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")( bulk = { case (entry, _) => entry.body.is_finished }, consume = { (args: List[(Entry, Boolean)]) => val results = db.transaction { for ((entry, strict) <- args) yield { if (progress.stopped) { entry.body.cancel() Exn.Res(()) } else if (entry.entry_name.readable(db)) { if (strict) { val msg = message("Duplicate export", entry.theory_name, entry.name) errors.change(msg :: _) } Exn.Res(()) } else Exn.capture { entry.write(db) } } } (results, true) }) def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = { if (!progress.stopped && !body.is_empty) { consumer.send(Export.make_entry(session_name, args, body, cache) -> args.strict) } } def shutdown(close: Boolean = false): List[String] = { consumer.shutdown() if (close) db.close() errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil) } } /* context for database access */ def open_database_context(store: Sessions.Store): Database_Context = { val database_server = if (store.database_server) Some(store.open_database_server()) else None new Database_Context(store, database_server) } def open_session_context0(store: Sessions.Store, session: String): Session_Context = open_database_context(store).open_session0(session, close_database_context = true) def open_session_context( store: Sessions.Store, session_base_info: Sessions.Base_Info, document_snapshot: Option[Document.Snapshot] = None ): Session_Context = { open_database_context(store).open_session( session_base_info, document_snapshot = document_snapshot, close_database_context = true) } class Database_Context private[Export]( val store: Sessions.Store, val database_server: Option[SQL.Database] ) extends AutoCloseable { database_context => override def toString: String = { val s = database_server match { case Some(db) => db.toString case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ") } "Database_Context(" + s + ")" } def cache: Term.Cache = store.cache def close(): Unit = database_server.foreach(_.close()) def open_output_database(session: String): Session_Database = database_server match { case Some(db) => new Session_Database(session, db) case None => new Session_Database(session, store.open_database(session, output = true)) { override def close(): Unit = db.close() } } def open_session0(session: String, close_database_context: Boolean = false): Session_Context = open_session(Sessions.base_info0(session), close_database_context = close_database_context) def open_session( session_base_info: Sessions.Base_Info, document_snapshot: Option[Document.Snapshot] = None, close_database_context: Boolean = false ): Session_Context = { val session_name = session_base_info.check.base.session_name val session_hierarchy = session_base_info.sessions_structure.build_hierarchy(session_name) val session_databases = database_server match { case Some(db) => session_hierarchy.map(name => new Session_Database(name, db)) case None => val attempts = session_hierarchy.map(name => name -> store.try_open_database(name, server = false)) attempts.collectFirst({ case (name, None) => name }) match { case Some(bad) => for ((_, Some(db)) <- attempts) db.close() store.error_database(bad) case None => for ((name, Some(db)) <- attempts) yield { new Session_Database(name, db) { override def close(): Unit = this.db.close() } } } } new Session_Context(database_context, session_base_info, session_databases, document_snapshot) { override def close(): Unit = { session_databases.foreach(_.close()) if (close_database_context) database_context.close() } } } } class Session_Database private[Export](val session: String, val db: SQL.Database) extends AutoCloseable { def close(): Unit = () lazy private [Export] val theory_names: List[String] = read_theory_names(db, session) lazy private [Export] val entry_names: List[Entry_Name] = read_entry_names(db, session) } class Session_Context private[Export]( val database_context: Database_Context, session_base_info: Sessions.Base_Info, db_hierarchy: List[Session_Database], document_snapshot: Option[Document.Snapshot] ) extends AutoCloseable { session_context => def close(): Unit = () def cache: Term.Cache = database_context.cache def sessions_structure: Sessions.Structure = session_base_info.sessions_structure def session_base: Sessions.Base = session_base_info.base def session_name: String = if (document_snapshot.isDefined) Sessions.DRAFT else session_base.session_name def session_database(session: String = session_name): Option[Session_Database] = db_hierarchy.find(_.session == session) def session_db(session: String = session_name): Option[SQL.Database] = session_database(session = session).map(_.db) def session_stack: List[String] = ((if (document_snapshot.isDefined) List(session_name) else Nil) ::: db_hierarchy.map(_.session)).reverse private def select[A]( session: String, select1: Entry_Name => Option[A], select2: Session_Database => List[A] ): List[A] = { def sel(name: String): List[A] = if (name == Sessions.DRAFT) { (for { snapshot <- document_snapshot.iterator entry_name <- snapshot.all_exports.keysIterator res <- select1(entry_name).iterator } yield entry_name -> res).toList.sortBy(_._1.compound_name).map(_._2) } else { session_database(name).map(select2).getOrElse(Nil) } if (session.nonEmpty) sel(session) else session_stack.flatMap(sel) } def entry_names(session: String = session_name): List[Entry_Name] = select(session, Some(_), _.entry_names) def theory_names(session: String = session_name): List[String] = select(session, a => if(a.name == THEORY_PARENTS) Some(a.theory) else None, _.theory_names) def get(theory: String, name: String): Option[Entry] = { def snapshot_entry: Option[Entry] = for { snapshot <- document_snapshot entry_name = Entry_Name(session = Sessions.DRAFT, theory = theory, name = name) entry <- snapshot.all_exports.get(entry_name) } yield entry def db_entry: Option[Entry] = db_hierarchy.view.map(database => Export.Entry_Name(session = database.session, theory = theory, name = name) .read(database.db, cache)) .collectFirst({ case Some(entry) => entry }) snapshot_entry orElse db_entry } def apply(theory: String, name: String, permissive: Boolean = false): Entry = get(theory, name) match { case None if permissive => empty_entry(theory, name) case None => error("Missing export entry " + quote(compound_name(theory, name))) case Some(entry) => entry } def theory(theory: String, other_cache: Option[Term.Cache] = None): Theory_Context = new Theory_Context(session_context, theory, other_cache) - def classpath(): List[File.Content_Bytes] = { + def classpath(): List[File.Content] = { (for { session <- session_stack.iterator info <- sessions_structure.get(session).iterator if info.export_classpath.nonEmpty matcher = make_matcher(info.export_classpath) entry_name <- entry_names(session = session).iterator if matcher(entry_name) entry <- get(entry_name.theory, entry_name.name).iterator - } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)).toList + } yield File.content(entry.entry_name.make_path(), entry.uncompressed)).toList } override def toString: String = "Export.Session_Context(" + commas_quote(session_stack) + ")" } class Theory_Context private[Export]( val session_context: Session_Context, val theory: String, other_cache: Option[Term.Cache] ) { def cache: Term.Cache = other_cache getOrElse session_context.cache def get(name: String): Option[Entry] = session_context.get(theory, name) def apply(name: String, permissive: Boolean = false): Entry = session_context.apply(theory, name, permissive = permissive) def uncompressed_yxml(name: String): XML.Body = get(name) match { case Some(entry) => entry.uncompressed_yxml case None => Nil } def document_id(): Option[Long] = apply(DOCUMENT_ID, permissive = true).text match { case Value.Long(id) => Some(id) case _ => None } def files(): Option[(String, List[String])] = split_lines(apply(FILES, permissive = true).text) match { case Nil => None case thy_file :: blobs_files => Some((thy_file, blobs_files)) } override def toString: String = "Export.Theory_Context(" + quote(theory) + ")" } /* export to file-system */ def export_files( store: Sessions.Store, session_name: String, export_dir: Path, progress: Progress = new Progress, export_prune: Int = 0, export_list: Boolean = false, export_patterns: List[String] = Nil ): Unit = { using(store.open_database(session_name)) { db => val entry_names = read_entry_names(db, session_name) // list if (export_list) { for (entry_name <- entry_names) progress.echo(entry_name.compound_name) } // export if (export_patterns.nonEmpty) { val matcher = make_matcher(export_patterns) for { entry_name <- entry_names if matcher(entry_name) entry <- entry_name.read(db, store.cache) } { val path = export_dir + entry_name.make_path(prune = export_prune) progress.echo("export " + path + (if (entry.executable) " (executable)" else "")) Isabelle_System.make_directory(path.dir) val bytes = entry.uncompressed if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes) File.set_executable(path, entry.executable) } } } } /* Isabelle tool wrapper */ val default_export_dir: Path = Path.explode("export") val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", Scala_Project.here, { args => /* arguments */ var export_dir = default_export_dir var dirs: List[Path] = Nil var export_list = false var no_build = false var options = Options.init() var export_prune = 0 var export_patterns: List[String] = Nil val getopts = Getopts(""" Usage: isabelle export [OPTIONS] SESSION Options are: -O DIR output directory for exported files (default: """ + default_export_dir + """) -d DIR include session directory -l list exports -n no build of session -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NUM prune path of exported files by NUM elements -x PATTERN extract files matching pattern (e.g. "*:**" for all) List or export theory exports for SESSION: named blobs produced by isabelle build. Option -l or -x is required; option -x may be repeated. The PATTERN language resembles glob patterns in the shell, with ? and * (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], and variants {pattern1,pattern2,pattern3}. """, "O:" -> (arg => export_dir = Path.explode(arg)), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "l" -> (_ => export_list = true), "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "p:" -> (arg => export_prune = Value.Int.parse(arg)), "x:" -> (arg => export_patterns ::= arg)) val more_args = getopts(args) val session_name = more_args match { case List(session_name) if export_list || export_patterns.nonEmpty => session_name case _ => getopts.usage() } val progress = new Console_Progress() /* build */ if (!no_build) { val rc = progress.interrupt_handler { Build.build_logic(options, session_name, progress = progress, dirs = dirs) } if (rc != Process_Result.RC.ok) sys.exit(rc) } /* export files */ val store = Sessions.store(options) export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune, export_list = export_list, export_patterns = export_patterns) }) } diff --git a/src/Pure/Thy/latex.scala b/src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala +++ b/src/Pure/Thy/latex.scala @@ -1,424 +1,424 @@ /* Title: Pure/Thy/latex.scala Author: Makarius Support for LaTeX. */ package isabelle import java.io.{File => JFile} import scala.annotation.tailrec import scala.collection.mutable import scala.collection.immutable.TreeMap import scala.util.matching.Regex object Latex { /* output name for LaTeX macros */ private val output_name_map: Map[Char, String] = Map('_' -> "UNDERSCORE", '\'' -> "PRIME", '0' -> "ZERO", '1' -> "ONE", '2' -> "TWO", '3' -> "THREE", '4' -> "FOUR", '5' -> "FIVE", '6' -> "SIX", '7' -> "SEVEN", '8' -> "EIGHT", '9' -> "NINE") def output_name(name: String): String = if (name.exists(output_name_map.keySet)) { val res = new StringBuilder for (c <- name) { output_name_map.get(c) match { case None => res += c case Some(s) => res ++= s } } res.toString } else name /* index entries */ def index_escape(str: String): String = { val special1 = "!\"@|" val special2 = "\\{}#" if (str.exists(c => special1.contains(c) || special2.contains(c))) { val res = new StringBuilder for (c <- str) { if (special1.contains(c)) { res ++= "\\char" res ++= Value.Int(c) } else { if (special2.contains(c)) { res += '"'} res += c } } res.toString } else str } object Index_Item { sealed case class Value(text: Text, like: String) def unapply(tree: XML.Tree): Option[Value] = tree match { case XML.Wrapped_Elem(Markup.Latex_Index_Item(_), text, like) => Some(Value(text, XML.content(like))) case _ => None } } object Index_Entry { sealed case class Value(items: List[Index_Item.Value], kind: String) def unapply(tree: XML.Tree): Option[Value] = tree match { case XML.Elem(Markup.Latex_Index_Entry(kind), body) => val items = body.map(Index_Item.unapply) if (items.forall(_.isDefined)) Some(Value(items.map(_.get), kind)) else None case _ => None } } /* tags */ object Tags { object Op extends Enumeration { val fold, drop, keep = Value } val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant" private def explode(spec: String): List[String] = Library.space_explode(',', spec) def apply(spec: String): Tags = new Tags(spec, (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op.Value]) { case (m, tag) => tag.toList match { case '/' :: cs => m + (cs.mkString -> Op.fold) case '-' :: cs => m + (cs.mkString -> Op.drop) case '+' :: cs => m + (cs.mkString -> Op.keep) case cs => m + (cs.mkString -> Op.keep) } }) val empty: Tags = apply("") } class Tags private(spec: String, map: TreeMap[String, Tags.Op.Value]) { override def toString: String = spec def get(name: String): Option[Tags.Op.Value] = map.get(name) def sty(comment_latex: Boolean): File.Content = { val path = Path.explode("isabelletags.sty") val comment = if (comment_latex) """\usepackage{comment}""" else """%plain TeX version of comment package -- much faster! \let\isafmtname\fmtname\def\fmtname{plain} \usepackage{comment} \let\fmtname\isafmtname""" val tags = (for ((name, op) <- map.iterator) yield "\\isa" + op + "tag{" + name + "}").toList - File.Content(path, comment + """ + File.content(path, comment + """ \newcommand{\isakeeptag}[1]% {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} \newcommand{\isadroptag}[1]% {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} \newcommand{\isafoldtag}[1]% {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}} """ + Library.terminate_lines(tags)) } } /* output text and positions */ type Text = XML.Body def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%\n" def init_position(file_pos: String): List[String] = if (file_pos.isEmpty) Nil else List("\\endinput\n", position(Markup.FILE, file_pos)) class Output(options: Options) { def latex_output(latex_text: Text): String = apply(latex_text) def latex_macro0(name: String, optional_argument: String = ""): Text = XML.string("\\" + name + optional_argument) def latex_macro(name: String, body: Text, optional_argument: String = ""): Text = XML.enclose("\\" + name + optional_argument + "{", "}", body) def latex_environment(name: String, body: Text, optional_argument: String = ""): Text = XML.enclose( "%\n\\begin{" + name + "}" + optional_argument + "%\n", "%\n\\end{" + name + "}", body) def latex_heading(kind: String, body: Text, optional_argument: String = ""): Text = XML.enclose( "%\n\\" + options.string("document_heading_prefix") + kind + optional_argument + "{", "%\n}\n", body) def latex_body(kind: String, body: Text, optional_argument: String = ""): Text = latex_environment("isamarkup" + kind, body, optional_argument) def latex_tag(name: String, body: Text, delim: Boolean = false): Text = { val s = output_name(name) val kind = if (delim) "delim" else "tag" val end = if (delim) "" else "{\\isafold" + s + "}%\n" if (options.bool("document_comment_latex")) { XML.enclose( "%\n\\begin{isa" + kind + s + "}\n", "%\n\\end{isa" + kind + s + "}\n" + end, body) } else { XML.enclose( "%\n\\isa" + kind + s + "\n", "%\n\\endisa" + kind + s + "\n" + end, body) } } def index_item(item: Index_Item.Value): String = { val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@" val text = index_escape(latex_output(item.text)) like + text } def index_entry(entry: Index_Entry.Value): Text = { val items = entry.items.map(index_item).mkString("!") val kind = if (entry.kind.isEmpty) "" else "|" + index_escape(entry.kind) latex_macro("index", XML.string(items + kind)) } /* standard output of text with per-line positions */ def unknown_elem(elem: XML.Elem, pos: Position.T): XML.Body = error("Unknown latex markup element " + quote(elem.name) + Position.here(pos) + ":\n" + XML.string_of_tree(elem)) def apply(latex_text: Text, file_pos: String = ""): String = { var line = 1 val result = new mutable.ListBuffer[String] val positions = new mutable.ListBuffer[String] ++= init_position(file_pos) val file_position = if (file_pos.isEmpty) Position.none else Position.File(file_pos) def traverse(xml: XML.Body): Unit = { xml.foreach { case XML.Text(s) => line += s.count(_ == '\n') result += s case elem @ XML.Elem(markup, body) => val a = Markup.Optional_Argument.get(markup.properties) traverse { markup match { case Markup.Document_Latex(props) => for (l <- Position.Line.unapply(props) if positions.nonEmpty) { val s = position(Value.Int(line), Value.Int(l)) if (positions.last != s) positions += s } body case Markup.Latex_Output(_) => XML.string(latex_output(body)) case Markup.Latex_Macro0(name) if body.isEmpty => latex_macro0(name, a) case Markup.Latex_Macro(name) => latex_macro(name, body, a) case Markup.Latex_Environment(name) => latex_environment(name, body, a) case Markup.Latex_Heading(kind) => latex_heading(kind, body, a) case Markup.Latex_Body(kind) => latex_body(kind, body, a) case Markup.Latex_Delim(name) => latex_tag(name, body, delim = true) case Markup.Latex_Tag(name) => latex_tag(name, body) case Markup.Latex_Index_Entry(_) => elem match { case Index_Entry(entry) => index_entry(entry) case _ => unknown_elem(elem, file_position) } case _ => unknown_elem(elem, file_position) } } } } traverse(latex_text) result ++= positions result.mkString } } /* generated .tex file */ private val File_Pattern = """^%:%file=(.+)%:%$""".r private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r def read_tex_file(tex_file: Path): Tex_File = { val positions = Line.logical_lines(File.read(tex_file)).reverse. takeWhile(_ != "\\endinput").reverse val source_file = positions match { case File_Pattern(file) :: _ => Some(file) case _ => None } val source_lines = if (source_file.isEmpty) Nil else positions.flatMap(line => line match { case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line) case _ => None }) new Tex_File(tex_file, source_file, source_lines) } final class Tex_File private[Latex]( tex_file: Path, source_file: Option[String], source_lines: List[(Int, Int)] ) { override def toString: String = tex_file.toString def source_position(l: Int): Option[Position.T] = source_file match { case None => None case Some(file) => val source_line = source_lines.iterator.takeWhile({ case (m, _) => m <= l }). foldLeft(0) { case (_, (_, n)) => n } if (source_line == 0) None else Some(Position.Line_File(source_line, file)) } def position(line: Int): Position.T = source_position(line) getOrElse Position.Line_File(line, tex_file.implode) } /* latex log */ def latex_errors(dir: Path, root_name: String): List[String] = { val root_log_path = dir + Path.explode(root_name).ext("log") if (root_log_path.is_file) { for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) } yield "Latex error" + Position.here(pos) + ":\n" + Library.indent_lines(2, msg) } else Nil } def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] = { val seen_files = Synchronized(Map.empty[JFile, Tex_File]) def check_tex_file(path: Path): Option[Tex_File] = seen_files.change_result(seen => seen.get(path.file) match { case None => if (path.is_file) { val tex_file = read_tex_file(path) (Some(tex_file), seen + (path.file -> tex_file)) } else (None, seen) case some => (some, seen) }) def tex_file_position(path: Path, line: Int): Position.T = check_tex_file(path) match { case Some(tex_file) => tex_file.position(line) case None => Position.Line_File(line, path.implode) } object File_Line_Error { val Pattern: Regex = """^(.*?\.\w\w\w):(\d+): (.*)$""".r def unapply(line: String): Option[(Path, Int, String)] = line match { case Pattern(file, Value.Int(line), message) => val path = File.standard_path(file) if (Path.is_wellformed(path)) { val file = (dir + Path.explode(path)).canonical val msg = Library.perhaps_unprefix("LaTeX Error: ", message) if (file.is_file) Some((file, line, msg)) else None } else None case _ => None } } val Line_Error = """^l\.\d+ (.*)$""".r val More_Error = List( "", "