diff --git a/src/Pure/PIDE/editor.scala b/src/Pure/PIDE/editor.scala --- a/src/Pure/PIDE/editor.scala +++ b/src/Pure/PIDE/editor.scala @@ -1,128 +1,118 @@ /* Title: Pure/PIDE/editor.scala Author: Makarius General editor operations. */ package isabelle abstract class Editor[Context] { /* PIDE session and document model */ def session: Session def flush(): Unit def invoke(): Unit def get_models(): Iterable[Document.Model] - /* bibtex */ - - def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document.Model)]] = - Bibtex.Entries.iterator(get_models()) - - def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset) - : Option[Completion.Result] = - Bibtex.completion(history, rendering, caret, get_models()) - - /* document editor */ protected val document_editor: Synchronized[Document_Editor.State] = Synchronized(Document_Editor.State()) protected def document_state(): Document_Editor.State = document_editor.value protected def document_state_changed(): Unit = {} private def document_state_change(f: Document_Editor.State => Document_Editor.State): Unit = { val changed = document_editor.change_result { st => val st1 = f(st) val changed = st.active_document_theories != st1.active_document_theories || st.selection != st1.selection (changed, st1) } if (changed) document_state_changed() } def document_session(): Option[Sessions.Background] = document_state().session_background def document_required(): List[Document.Node.Name] = { val st = document_state() if (st.is_active) { for { a <- st.all_document_theories b = session.resources.migrate_name(a) if st.selection(b) } yield b } else Nil } def document_node_required(name: Document.Node.Name): Boolean = { val st = document_state() st.is_active && st.selection.contains(name) && st.all_document_theories.exists(a => session.resources.migrate_name(a) == name) } def document_theories(): List[Document.Node.Name] = document_state().active_document_theories.map(session.resources.migrate_name) def document_selection(): Set[Document.Node.Name] = document_state().selection def document_setup(background: Option[Sessions.Background]): Unit = document_state_change(_.copy(session_background = background)) def document_select( names: Iterable[Document.Node.Name], set: Boolean = false, toggle: Boolean = false ): Unit = document_state_change(_.select(names, set = set, toggle = toggle)) def document_select_all(set: Boolean = false): Unit = document_state_change { st => val domain = st.active_document_theories.map(session.resources.migrate_name) st.select(domain, set = set) } def document_init(id: AnyRef): Unit = document_state_change(_.register_view(id)) def document_exit(id: AnyRef): Unit = document_state_change(_.unregister_view(id)) /* current situation */ def current_node(context: Context): Option[Document.Node.Name] def current_node_snapshot(context: Context): Option[Document.Snapshot] def node_snapshot(name: Document.Node.Name): Document.Snapshot def current_command(context: Context, snapshot: Document.Snapshot): Option[Command] /* overlays */ def node_overlays(name: Document.Node.Name): Document.Node.Overlays def insert_overlay(command: Command, fn: String, args: List[String]): Unit def remove_overlay(command: Command, fn: String, args: List[String]): Unit /* hyperlinks */ abstract class Hyperlink { def external: Boolean = false def follow(context: Context): Unit } def hyperlink_command( focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0) : Option[Hyperlink] /* dispatcher thread */ def assert_dispatcher[A](body: => A): A def require_dispatcher[A](body: => A): A def send_dispatcher(body: => Unit): Unit def send_wait_dispatcher(body: => Unit): Unit } diff --git a/src/Pure/PIDE/rendering.scala b/src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala +++ b/src/Pure/PIDE/rendering.scala @@ -1,773 +1,762 @@ /* Title: Pure/PIDE/rendering.scala Author: Makarius Isabelle-specific implementation of quasi-abstract rendering and markup interpretation. */ package isabelle import java.io.{File => JFile} import java.nio.file.FileSystems import scala.collection.immutable.SortedMap object Rendering { /* color */ object Color extends Enumeration { // background val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result, markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value val background_colors: ValueSet = values // foreground val quoted, antiquoted = Value val foreground_colors: ValueSet = values -- background_colors // message underline val writeln, information, warning, legacy, error = Value val message_underline_colors: ValueSet = values -- background_colors -- foreground_colors // message background val writeln_message, information_message, tracing_message, warning_message, legacy_message, error_message = Value val message_background_colors: ValueSet = values -- background_colors -- foreground_colors -- message_underline_colors // text val main, keyword1, keyword2, keyword3, quasi_keyword, improper, operator, tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted, inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter, antiquote, raw_text, plain_text = Value val text_colors: ValueSet = values -- background_colors -- foreground_colors -- message_underline_colors -- message_background_colors // text overview val unprocessed, running = Value val text_overview_colors = Set(unprocessed, running, error, warning) } /* output messages */ val state_pri = 1 val writeln_pri = 2 val information_pri = 3 val tracing_pri = 4 val warning_pri = 5 val legacy_pri = 6 val error_pri = 7 val message_pri = Map( Markup.STATE -> state_pri, Markup.STATE_MESSAGE -> state_pri, Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri, Markup.INFORMATION -> information_pri, Markup.INFORMATION_MESSAGE -> information_pri, Markup.TRACING -> tracing_pri, Markup.TRACING_MESSAGE -> tracing_pri, Markup.WARNING -> warning_pri, Markup.WARNING_MESSAGE -> warning_pri, Markup.LEGACY -> legacy_pri, Markup.LEGACY_MESSAGE -> legacy_pri, Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri ).withDefaultValue(0) val message_underline_color = Map( writeln_pri -> Color.writeln, information_pri -> Color.information, warning_pri -> Color.warning, legacy_pri -> Color.legacy, error_pri -> Color.error) val message_background_color = Map( writeln_pri -> Color.writeln_message, information_pri -> Color.information_message, tracing_pri -> Color.tracing_message, warning_pri -> Color.warning_message, legacy_pri -> Color.legacy_message, error_pri -> Color.error_message) def output_messages(results: Command.Results, output_state: Boolean): List[XML.Elem] = { val (states, other) = results.iterator.map(_._2).filterNot(Protocol.is_result).toList .partition(Protocol.is_state) (if (output_state) states else Nil) ::: other } /* text color */ val text_color = Map( Markup.KEYWORD1 -> Color.keyword1, Markup.KEYWORD2 -> Color.keyword2, Markup.KEYWORD3 -> Color.keyword3, Markup.QUASI_KEYWORD -> Color.quasi_keyword, Markup.IMPROPER -> Color.improper, Markup.OPERATOR -> Color.operator, Markup.STRING -> Color.main, Markup.ALT_STRING -> Color.main, Markup.CARTOUCHE -> Color.main, Markup.LITERAL -> Color.keyword1, Markup.DELIMITER -> Color.main, Markup.TFREE -> Color.tfree, Markup.TVAR -> Color.tvar, Markup.FREE -> Color.free, Markup.SKOLEM -> Color.skolem, Markup.BOUND -> Color.bound, Markup.VAR -> Color.`var`, Markup.INNER_STRING -> Color.inner_quoted, Markup.INNER_CARTOUCHE -> Color.inner_cartouche, Markup.DYNAMIC_FACT -> Color.dynamic, Markup.CLASS_PARAMETER -> Color.class_parameter, Markup.ANTIQUOTE -> Color.antiquote, Markup.RAW_TEXT -> Color.raw_text, Markup.PLAIN_TEXT -> Color.plain_text, Markup.ML_KEYWORD1 -> Color.keyword1, Markup.ML_KEYWORD2 -> Color.keyword2, Markup.ML_KEYWORD3 -> Color.keyword3, Markup.ML_DELIMITER -> Color.main, Markup.ML_NUMERAL -> Color.inner_numeral, Markup.ML_CHAR -> Color.inner_quoted, Markup.ML_STRING -> Color.inner_quoted, Markup.ML_COMMENT -> Color.comment1, Markup.COMMENT -> Color.comment1, Markup.COMMENT1 -> Color.comment1, Markup.COMMENT2 -> Color.comment2, Markup.COMMENT3 -> Color.comment3) val foreground = Map( Markup.STRING -> Color.quoted, Markup.ALT_STRING -> Color.quoted, Markup.CARTOUCHE -> Color.quoted, Markup.ANTIQUOTED -> Color.antiquoted) /* tooltips */ val tooltip_descriptions = Map( - Markup.CITATION -> "citation", Markup.TOKEN_RANGE -> "inner syntax token", Markup.FREE -> "free variable", Markup.SKOLEM -> "skolem variable", Markup.BOUND -> "bound variable", Markup.VAR -> "schematic variable", Markup.TFREE -> "free type variable", Markup.TVAR -> "schematic type variable") /* entity focus */ object Focus { def apply(ids: Set[Long]): Focus = new Focus(ids) val empty: Focus = apply(Set.empty) def make(args: List[Text.Info[Focus]]): Focus = args.foldLeft(empty) { case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 } val full: Focus = new Focus(Set.empty) { override def apply(id: Long): Boolean = true override def toString: String = "Focus.full" } } sealed class Focus private[Rendering](protected val rep: Set[Long]) { def defined: Boolean = rep.nonEmpty def apply(id: Long): Boolean = rep.contains(id) def + (id: Long): Focus = if (rep.contains(id)) this else new Focus(rep + id) def ++ (other: Focus): Focus = if (this eq other) this else if (rep.isEmpty) other else other.rep.iterator.foldLeft(this)(_ + _) override def toString: String = rep.mkString("Focus(", ",", ")") } /* markup elements */ val position_elements = Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) val semantic_completion_elements = Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) val language_context_elements = Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE, Markup.ML_STRING, Markup.ML_COMMENT) val language_elements = Markup.Elements(Markup.LANGUAGE) - val citation_elements = Markup.Elements(Markup.CITATION) - val active_elements = Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.THEORY_EXPORTS, Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL) val background_elements = Document_Status.Command_Status.proper_elements + Markup.WRITELN_MESSAGE + Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY + Markup.ENTITY + Markup.Markdown_Bullet.name ++ active_elements val foreground_elements = Markup.Elements(foreground.keySet) val text_color_elements = Markup.Elements(text_color.keySet) val tooltip_elements = Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet) val tooltip_message_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, Markup.BAD) val message_elements = Markup.Elements(message_pri.keySet) val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY) val error_elements = Markup.Elements(Markup.ERROR) val entity_elements = Markup.Elements(Markup.ENTITY) val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED) val meta_data_elements = Markup.Elements(Markup.META_TITLE, Markup.META_CREATOR, Markup.META_CONTRIBUTOR, Markup.META_DATE, Markup.META_DESCRIPTION, Markup.META_LICENSE) val document_tag_elements = Markup.Elements(Markup.Document_Tag.name) val markdown_elements = Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name, Markup.Markdown_Bullet.name) } class Rendering( val snapshot: Document.Snapshot, val options: Options, val session: Session ) { override def toString: String = "Rendering(" + snapshot.toString + ")" def get_text(range: Text.Range): Option[String] = None /* caret */ def before_caret_range(caret: Text.Offset): Text.Range = { val former_caret = snapshot.revert(caret) snapshot.convert(Text.Range(former_caret - 1, former_caret)) } /* completion */ def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range) : Option[Text.Info[Completion.Semantic]] = if (snapshot.is_outdated) None else { snapshot.select(caret_range, Rendering.semantic_completion_elements, _ => { case Completion.Semantic.Info(info) => completed_range match { case Some(range0) if range0.contains(info.range) && range0 != info.range => None case _ => Some(info) } case _ => None }).headOption.map(_.info) } def semantic_completion_result( history: Completion.History, unicode: Boolean, completed_range: Option[Text.Range], caret_range: Text.Range ): (Boolean, Option[Completion.Result]) = { semantic_completion(completed_range, caret_range) match { case Some(Text.Info(_, Completion.No_Completion)) => (true, None) case Some(Text.Info(range, names: Completion.Names)) => get_text(range) match { case Some(original) => (false, names.complete(range, history, unicode, original)) case None => (false, None) } case None => (false, None) } } def language_context(range: Text.Range): Option[Completion.Language_Context] = snapshot.select(range, Rendering.language_context_elements, _ => { case Text.Info(_, XML.Elem(Markup.Language(lang), _)) => if (lang.delimited) Some(Completion.Language_Context(lang)) else None case Text.Info(_, elem) if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT => Some(Completion.Language_Context.ML_inner) case Text.Info(_, _) => Some(Completion.Language_Context.inner) }).headOption.map(_.info) - def citations(range: Text.Range): List[Text.Info[String]] = - snapshot.select(range, Rendering.citation_elements, _ => - { - case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => - Some(Text.Info(snapshot.convert(info_range), name)) - case _ => None - }).map(_.info) - /* file-system path completion */ def language_path(range: Text.Range): Option[Text.Info[Boolean]] = snapshot.select(range, Rendering.language_elements, _ => { case Text.Info(info_range, XML.Elem(Markup.Language(lang), _)) if lang.is_path => Some((lang.delimited, snapshot.convert(info_range))) case _ => None }).headOption.map({ case Text.Info(_, (delimited, range)) => Text.Info(range, delimited) }) def path_completion(caret: Text.Offset): Option[Completion.Result] = { def complete(text: String): List[(String, List[String])] = { try { val path = Path.explode(text) val (dir, base_name) = if (text == "" || text.endsWith("/")) (path, "") else (path.dir, path.file_name) val directory = new JFile(session.resources.append_path(snapshot.node_name.master_dir, dir)) val files = directory.listFiles if (files == null) Nil else { val ignore = space_explode(':', options.string("completion_path_ignore")). map(s => FileSystems.getDefault.getPathMatcher("glob:" + s)) (for { file <- files.iterator name = file.getName if name.startsWith(base_name) path_name = new JFile(name).toPath if !ignore.exists(matcher => matcher.matches(path_name)) text1 = (dir + Path.basic(name)).implode_short if text != text1 is_dir = new JFile(directory, name).isDirectory replacement = text1 + (if (is_dir) "/" else "") descr = List(text1, if (is_dir) "(directory)" else "(file)") } yield (replacement, descr)).take(options.int("completion_limit")).toList } } catch { case ERROR(_) => Nil } } def is_wrapped(s: String): Boolean = s.startsWith("\"") && s.endsWith("\"") || s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded) for { Text.Info(r1, delimited) <- language_path(before_caret_range(caret)) s1 <- get_text(r1) (r2, s2) <- if (is_wrapped(s1)) { Some((Text.Range(r1.start + 1, r1.stop - 1), s1.substring(1, s1.length - 1))) } else if (delimited) Some((r1, s1)) else None if Path.is_valid(s2) paths = complete(s2) if paths.nonEmpty items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false)) } yield Completion.Result(r2, s2, false, items) } /* spell checker */ lazy val spell_checker_include: Markup.Elements = Markup.Elements(space_explode(',', options.string("spell_checker_include")): _*) lazy val spell_checker_exclude: Markup.Elements = Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*) lazy val spell_checker_elements: Markup.Elements = spell_checker_include ++ spell_checker_exclude def spell_checker(range: Text.Range): List[Text.Info[Text.Range]] = { val result = snapshot.select(range, spell_checker_elements, _ => { case info => Some( if (spell_checker_include(info.info.name)) Some(snapshot.convert(info.range)) else None) }) for (Text.Info(range, Some(range1)) <- result) yield Text.Info(range, range1) } def spell_checker_point(range: Text.Range): Option[Text.Range] = spell_checker(range).headOption.map(_.info) /* text background */ def background( elements: Markup.Elements, range: Text.Range, focus: Rendering.Focus ) : List[Text.Info[Rendering.Color.Value]] = { for { Text.Info(r, result) <- snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])]( range, (List(Markup.Empty), None), elements, command_states => { case ((markups, color), Text.Info(_, XML.Elem(markup, _))) if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) => Some((markup :: markups, color)) case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) => Some((Nil, Some(Rendering.Color.bad))) case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => Some((Nil, Some(Rendering.Color.intensify))) case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) => Some((Nil, Some(Rendering.Color.entity))) case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) => val color = depth % 4 match { case 1 => Rendering.Color.markdown_bullet1 case 2 => Rendering.Color.markdown_bullet2 case 3 => Rendering.Color.markdown_bullet3 case _ => Rendering.Color.markdown_bullet4 } Some((Nil, Some(color))) case (_, Text.Info(_, Protocol.Dialog(_, serial, result))) => command_states.collectFirst( { case st if st.results.defined(serial) => st.results.get(serial).get }) match { case Some(Protocol.Dialog_Result(res)) if res == result => Some((Nil, Some(Rendering.Color.active_result))) case _ => Some((Nil, Some(Rendering.Color.active))) } case (_, Text.Info(_, elem)) => if (Rendering.active_elements(elem.name)) Some((Nil, Some(Rendering.Color.active))) else None }) color <- result match { case (markups, opt_color) if markups.nonEmpty => val status = Document_Status.Command_Status.make(markups.iterator) if (status.is_unprocessed) Some(Rendering.Color.unprocessed1) else if (status.is_running) Some(Rendering.Color.running1) else if (status.is_canceled) Some(Rendering.Color.canceled) else opt_color case (_, opt_color) => opt_color } } yield Text.Info(r, color) } /* text foreground */ def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = snapshot.select(range, Rendering.foreground_elements, _ => { case info => Some(Rendering.foreground(info.info.name)) }) /* entity focus */ def entity_focus_defs(range: Text.Range): Rendering.Focus = Rendering.Focus.make( snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ => { case (focus, Text.Info(_, XML.Elem(Markup.Entity.Def(i), _))) => Some(focus + i) case _ => None })) def entity_focus(range: Text.Range, defs_focus: Rendering.Focus): Rendering.Focus = Rendering.Focus.make( snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ => { case (focus, Text.Info(_, XML.Elem(Markup.Entity.Ref(i), _))) if defs_focus(i) => Some(focus + i) case _ => None })) /* caret focus */ def caret_focus(caret_range: Text.Range, defs_range: Text.Range): Rendering.Focus = { val focus = entity_focus_defs(caret_range) if (focus.defined) focus else if (defs_range == Text.Range.offside) Rendering.Focus.empty else { val defs_focus = if (defs_range == Text.Range.full) Rendering.Focus.full else entity_focus_defs(defs_range) entity_focus(caret_range, defs_focus) } } def caret_focus_ranges(caret_range: Text.Range, defs_range: Text.Range): List[Text.Range] = { val focus = caret_focus(caret_range, defs_range) if (focus.defined) { snapshot.cumulate[Boolean](defs_range, false, Rendering.entity_elements, _ => { case (_, Text.Info(_, XML.Elem(Markup.Entity.Occ(i), _))) if focus(i) => Some(true) case _ => None }).flatMap(info => if (info.info) Some(info.range) else None) } else Nil } /* messages */ def message_underline_color( elements: Markup.Elements, range: Text.Range ) : List[Text.Info[Rendering.Color.Value]] = { val results = snapshot.cumulate[Int](range, 0, elements, _ => { case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) }) for { Text.Info(r, pri) <- results color <- Rendering.message_underline_color.get(pri) } yield Text.Info(r, color) } def text_messages(range: Text.Range): List[Text.Info[XML.Elem]] = { val results = snapshot.cumulate[Vector[Command.Results.Entry]]( range, Vector.empty, Rendering.message_elements, command_states => { case (res, Text.Info(_, elem)) => Command.State.get_result_proper(command_states, elem.markup.properties) .map(res :+ _) }) var seen_serials = Set.empty[Long] def seen(i: Long): Boolean = { val b = seen_serials(i) seen_serials += i b } for { Text.Info(range, entries) <- results (i, elem) <- entries if !seen(i) } yield Text.Info(range, elem) } /* tooltips */ def timing_threshold: Double = 0.0 private sealed case class Tooltip_Info( range: Text.Range, timing: Timing = Timing.zero, messages: List[(Long, XML.Tree)] = Nil, rev_infos: List[(Boolean, XML.Tree)] = Nil ) { def + (t: Timing): Tooltip_Info = copy(timing = timing + t) def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info = { val r = snapshot.convert(r0) if (range == r) copy(messages = (serial -> tree) :: messages) else copy(range = r, messages = List(serial -> tree)) } def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info = { val r = snapshot.convert(r0) if (range == r) copy(rev_infos = (important -> tree) :: rev_infos) else copy (range = r, rev_infos = List(important -> tree)) } def timing_info(tree: XML.Tree): Option[XML.Tree] = tree match { case XML.Elem(Markup(Markup.TIMING, _), _) => if (timing.elapsed.seconds >= timing_threshold) Some(XML.Text(timing.message)) else None case _ => Some(tree) } def infos(important: Boolean): List[XML.Tree] = for { (is_important, tree) <- rev_infos.reverse if is_important == important tree1 <- timing_info(tree) } yield tree1 } def perhaps_append_file(node_name: Document.Node.Name, name: String): String = if (Path.is_valid(name)) session.resources.append_path(node_name.master_dir, Path.explode(name)) else name def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = { val results = snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states => { case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t) case (info, Text.Info(r0, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body))) if body.nonEmpty => Some(info + (r0, i, msg)) case (info, Text.Info(r0, XML.Elem(Markup(name, props), _))) if Rendering.tooltip_message_elements(name) => for ((i, tree) <- Command.State.get_result_proper(command_states, props)) yield (info + (r0, i, tree)) case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _))) if kind != "" && kind != Markup.ML_DEF => val kind1 = Word.implode(Word.explode('_', kind)) val txt1 = if (name == "") kind1 else if (kind1 == "") quote(name) else kind1 + " " + quote(name) val info1 = info + (r0, true, XML.Text(txt1)) Some(if (kind == Markup.COMMAND) info1 + (r0, true, XML.elem(Markup.TIMING)) else info1) case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) => val file = perhaps_append_file(snapshot.node_name, name) val text = if (name == file) "file " + quote(file) else "path " + quote(name) + "\nfile " + quote(file) Some(info + (r0, true, XML.Text(text))) case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) => val text = "doc " + quote(name) Some(info + (r0, true, XML.Text(text))) case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) => Some(info + (r0, true, XML.Text("URL " + quote(name)))) case (info, Text.Info(r0, XML.Elem(Markup(name, _), body))) if name == Markup.SORTING || name == Markup.TYPING => Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body))) case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) => Some(info + (r0, true, Pretty.block(body, indent = 0))) case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body))) case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) => val text = if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" else "breakpoint (disabled)" Some(info + (r0, true, XML.Text(text))) case (info, Text.Info(r0, XML.Elem(Markup.Language(lang), _))) => Some(info + (r0, true, XML.Text("language: " + lang.description))) case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) => val descr = if (kind == "") "expression" else "expression: " + kind Some(info + (r0, true, XML.Text(descr))) case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => Some(info + (r0, true, XML.Text("Markdown: paragraph"))) case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), _))) => Some(info + (r0, true, XML.Text("Markdown: item"))) case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) => Some(info + (r0, true, XML.Text("Markdown: " + kind))) case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) => Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc))) }).map(_.info) if (results.isEmpty) None else { val r = Text.Range(results.head.range.start, results.last.range.stop) val all_tips = results.flatMap(_.messages).foldLeft(SortedMap.empty[Long, XML.Tree])(_ + _) .iterator.map(_._2).toList ::: results.flatMap(res => res.infos(true)) ::: results.flatMap(res => res.infos(false)).lastOption.toList if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips)) } } /* messages */ def warnings(range: Text.Range): List[Text.Markup] = snapshot.select(range, Rendering.warning_elements, _ => Some(_)).map(_.info) def errors(range: Text.Range): List[Text.Markup] = snapshot.select(range, Rendering.error_elements, _ => Some(_)).map(_.info) /* command status overview */ def overview_color(range: Text.Range): Option[Rendering.Color.Value] = { if (snapshot.is_outdated) None else { val results = snapshot.cumulate[List[Markup]](range, Nil, Document_Status.Command_Status.liberal_elements, _ => { case (status, Text.Info(_, elem)) => Some(elem.markup :: status) }, status = true) if (results.isEmpty) None else { val status = Document_Status.Command_Status.make(results.iterator.flatMap(_.info)) if (status.is_running) Some(Rendering.Color.running) else if (status.is_failed) Some(Rendering.Color.error) else if (status.is_warned) Some(Rendering.Color.warning) else if (status.is_unprocessed) Some(Rendering.Color.unprocessed) else None } } } /* antiquoted text */ def antiquoted(range: Text.Range): Option[Text.Range] = snapshot.cumulate[Option[Text.Range]](range, None, Rendering.antiquoted_elements, _ => { case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None }).headOption.flatMap(_.info) /* meta data */ def meta_data(range: Text.Range): Properties.T = { val results = snapshot.cumulate[Properties.T](range, Nil, Rendering.meta_data_elements, _ => { case (res, Text.Info(_, elem)) => val plain_text = XML.content(elem) Some((elem.name -> plain_text) :: res) }) Library.distinct(results.flatMap(_.info.reverse)) } /* document tags */ def document_tags(range: Text.Range): List[String] = { val results = snapshot.cumulate[List[String]](range, Nil, Rendering.document_tag_elements, _ => { case (res, Text.Info(_, XML.Elem(Markup.Document_Tag(name), _))) => Some(name :: res) case _ => None }) Library.distinct(results.flatMap(_.info.reverse)) } } diff --git a/src/Pure/Thy/bibtex.ML b/src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML +++ b/src/Pure/Thy/bibtex.ML @@ -1,130 +1,127 @@ (* Title: Pure/Thy/bibtex.ML Author: Makarius BibTeX support. *) signature BIBTEX = sig val check_database: Position.T -> string -> (string * Position.T) list * (string * Position.T) list val check_database_output: Position.T -> string -> unit val check_bibtex_entry: Proof.context -> string * Position.T -> unit val cite_macro: string Config.T val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory end; structure Bibtex: BIBTEX = struct (* check database *) type message = string * Position.T; fun check_database pos0 database = \<^scala>\bibtex_check_database\ database |> YXML.parse_body |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0)); fun check_database_output pos0 database = let val (errors, warnings) = check_database pos0 database in errors |> List.app (fn (msg, pos) => Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n " ^ msg)); warnings |> List.app (fn (msg, pos) => warning ("Bibtex warning" ^ Position.here pos ^ ":\n " ^ msg)) end; (* check bibtex entry *) fun check_bibtex_entry ctxt (name, pos) = let fun warn () = if Context_Position.is_visible ctxt then warning ("Unknown session context: cannot check Bibtex entry " ^ quote name ^ Position.here pos) else (); in if name = "*" then () else (case Position.id_of pos of NONE => warn () | SOME id => (case \<^scala>\bibtex_session_entries\ [id] of [] => warn () | _ :: entries => Completion.check_entity Markup.bibtex_entryN (map (rpair Position.none) entries) ctxt (name, pos) |> ignore)) end; (* document antiquotations *) val cite_macro = Attrib.setup_config_string \<^binding>\cite_macro\ (K ""); fun get_cite_macro ctxt = Config.get ctxt cite_macro; val _ = Theory.setup (Document_Antiquotation.setup_option \<^binding>\cite_macro\ (Config.put cite_macro)); local val parse_citations = Parse.and_list1 Args.name_position; fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) = let val loc = the_default Input.empty opt_loc; - val _ = - Context_Position.reports ctxt - (Document_Output.document_reports loc @ - map (fn (name, pos) => (pos, Markup.citation name)) citations); + val _ = Context_Position.reports ctxt (Document_Output.document_reports loc); val _ = List.app (check_bibtex_entry ctxt) citations; val kind = if macro_name = "" then get_kind ctxt else macro_name; val location = Document_Output.output_document ctxt {markdown = false} loc; in Latex.cite {kind = kind, citations = citations, location = location} end; fun cite_command_old ctxt get_kind args = let val _ = if Context_Position.is_visible ctxt then legacy_feature ("Old antiquotation syntax, better use \"isabelle update -u cite\"" ^ Position.here_list (map snd (snd args))) else (); in cite_command ctxt get_kind (args, "") end; val cite_keywords = Thy_Header.bootstrap_keywords |> Keyword.add_keywords (map (fn a => ((a, Position.none), Keyword.no_spec)) ["in", "using"]); fun cite_command_embedded ctxt get_kind input = let val parser = Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations -- Scan.optional (Parse.$$$ "using" |-- Parse.!!! Parse.name) ""; val args = Parse.read_embedded ctxt cite_keywords parser input; in cite_command ctxt get_kind args end; fun cite_command_parser get_kind = Scan.option Args.cartouche_input -- parse_citations >> (fn args => fn ctxt => cite_command_old ctxt get_kind args) || Parse.embedded_input >> (fn arg => fn ctxt => cite_command_embedded ctxt get_kind arg); in fun cite_antiquotation binding get_kind = Document_Output.antiquotation_raw binding (Scan.lift (cite_command_parser get_kind)) (fn ctxt => fn cmd => cmd ctxt); end; val _ = Theory.setup (cite_antiquotation \<^binding>\cite\ get_cite_macro #> cite_antiquotation \<^binding>\nocite\ (K "nocite") #> cite_antiquotation \<^binding>\citet\ (K "citet") #> cite_antiquotation \<^binding>\citep\ (K "citep")); end; diff --git a/src/Pure/Thy/bibtex.scala b/src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala +++ b/src/Pure/Thy/bibtex.scala @@ -1,896 +1,855 @@ /* Title: Pure/Thy/bibtex.scala Author: Makarius BibTeX support. */ package isabelle import java.io.{File => JFile} import scala.collection.mutable import scala.util.parsing.combinator.RegexParsers import scala.util.parsing.input.Reader import scala.util.matching.Regex import isabelle.{Token => Isar_Token} object Bibtex { /** file format **/ class File_Format extends isabelle.File_Format { val format_name: String = "bibtex" val file_ext: String = "bib" override def parse_data(name: String, text: String): Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = name) override def theory_suffix: String = "bibtex_file" override def theory_content(name: String): String = """theory "bib" imports Pure begin bibtex_file "." end""" override def theory_excluded(name: String): Boolean = name == "bib" override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = { val name = snapshot.node_name if (detect(name.node)) { val title = "Bibliography " + quote(snapshot.node_name.file_name) val content = Isabelle_System.with_tmp_file("bib", "bib") { bib => File.write(bib, snapshot.node.source) Bibtex.html_output(List(bib), style = "unsort", title = title) } Some(Browser_Info.HTML_Document(title, content)) } else None } } /** bibtex errors **/ def bibtex_errors(dir: Path, root_name: String): List[String] = { val log_path = dir + Path.explode(root_name).ext("blg") if (log_path.is_file) { val Error1 = """^(I couldn't open database file .+)$""".r val Error2 = """^(I found no .+)$""".r val Error3 = """^(.+)---line (\d+) of file (.+)""".r Line.logical_lines(File.read(log_path)).flatMap(line => line match { case Error1(msg) => Some("Bibtex error: " + msg) case Error2(msg) => Some("Bibtex error: " + msg) case Error3(msg, Value.Int(l), file) => val path = File.standard_path(file) if (Path.is_wellformed(path)) { val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode) Some("Bibtex error" + Position.here(pos) + ":\n " + msg) } else None case _ => None }) } else Nil } /** check database **/ def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) = { val chunks = parse(Line.normalize(database)) var chunk_pos = Map.empty[String, Position.T] val tokens = new mutable.ListBuffer[(Token, Position.T)] var line = 1 var offset = 1 def make_pos(length: Int): Position.T = Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line) def advance_pos(tok: Token): Unit = { for (s <- Symbol.iterator(tok.source)) { if (Symbol.is_newline(s)) line += 1 offset += 1 } } def get_line_pos(l: Int): Position.T = if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none for (chunk <- chunks) { val name = chunk.name if (name != "" && !chunk_pos.isDefinedAt(name)) { chunk_pos += (name -> make_pos(chunk.heading_length)) } for (tok <- chunk.tokens) { tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length)) advance_pos(tok) } } Isabelle_System.with_tmp_dir("bibtex") { tmp_dir => File.write(tmp_dir + Path.explode("root.bib"), tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n")) File.write(tmp_dir + Path.explode("root.aux"), "\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}") Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file) val Error = """^(.*)---line (\d+) of file root.bib$""".r val Warning = """^Warning--(.+)$""".r val Warning_Line = """--line (\d+) of file root.bib$""".r val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r val log_file = tmp_dir + Path.explode("root.blg") val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil val (errors, warnings) = if (lines.isEmpty) (Nil, Nil) else { lines.zip(lines.tail ::: List("")).flatMap( { case (Error(msg, Value.Int(l)), _) => Some((true, (msg, get_line_pos(l)))) case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) => Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name)))) case (Warning(msg), Warning_Line(Value.Int(l))) => Some((false, (Word.capitalize(msg), get_line_pos(l)))) case (Warning(msg), _) => Some((false, (Word.capitalize(msg), Position.none))) case _ => None } ).partition(_._1) } (errors.map(_._2), warnings.map(_._2)) } } object Check_Database extends Scala.Fun_String("bibtex_check_database") { val here = Scala_Project.here def apply(database: String): String = { import XML.Encode._ YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))( check_database(database))) } } /** document model **/ /* entries */ object Entries { val empty: Entries = apply(Nil) def apply(entries: List[Text.Info[String]], errors: List[String] = Nil): Entries = new Entries(entries, errors) def parse(text: String, file_pos: String = ""): Entries = { val entries = new mutable.ListBuffer[Text.Info[String]] var offset = 0 var line = 1 var err_line = 0 try { for (chunk <- Bibtex.parse(text)) { val end_offset = offset + chunk.source.length if (chunk.name != "" && !chunk.is_command) { entries += Text.Info(Text.Range(offset, end_offset), chunk.name) } if (chunk.is_malformed && err_line == 0) { err_line = line } offset = end_offset line += Library.count_newlines(chunk.source) } val err_pos = if (err_line == 0 || file_pos.isEmpty) Position.none else Position.Line_File(err_line, file_pos) val errors = if (err_line == 0) Nil else List("Malformed bibtex file" + Position.here(err_pos)) apply(entries.toList, errors = errors) } catch { case ERROR(msg) => apply(Nil, errors = List(msg)) } } - - def iterator[A <: Document.Model](models: Iterable[A]): Iterator[Text.Info[(String, A)]] = - for { - model <- models.iterator - bibtex_entries <- model.get_data(classOf[Entries]).iterator - info <- bibtex_entries.entries.iterator - } yield info.map((_, model)) } final class Entries private(val entries: List[Text.Info[String]], val errors: List[String]) { override def toString: String = "Bibtex.Entries(" + entries.length + ")" def ::: (other: Entries): Entries = new Entries(entries ::: other.entries, errors ::: other.errors) } object Session_Entries extends Scala.Fun("bibtex_session_entries") { val here = Scala_Project.here override def invoke(session: Session, args: List[Bytes]): List[Bytes] = { val sessions = session.resources.sessions_structure val id = Value.Long.parse(Library.the_single(args).text) val qualifier = session.get_state().lookup_id(id) match { case None => Sessions.DRAFT case Some(st) => sessions.theory_qualifier(st.command.node_name.theory) } val res = if (qualifier == Sessions.DRAFT || !sessions.defined(qualifier)) Nil else qualifier :: sessions(qualifier).bibtex_entries.entries.map(_.info) res.map(Bytes.apply) } } - /* completion */ - - def completion[A <: Document.Model]( - history: Completion.History, - rendering: Rendering, - caret: Text.Offset, - models: Iterable[A] - ): Option[Completion.Result] = { - for { - Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption - name1 <- Completion.clean_name(name) - - original <- rendering.get_text(r) - original1 <- Completion.clean_name(Library.perhaps_unquote(original)) - - entries = - (for { - Text.Info(_, (entry, _)) <- Entries.iterator(models) - if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1 - } yield entry).toList - if entries.nonEmpty - - items = - entries.sorted.map({ - case entry => - val full_name = Long_Name.qualify(Markup.CITATION, entry) - val description = List(entry, "(BibTeX entry)") - val replacement = quote(entry) - Completion.Item(r, original, full_name, description, replacement, 0, false) - }).sorted(history.ordering).take(rendering.options.int("completion_limit")) - } yield Completion.Result(r, original, false, items) - } - - /** content **/ private val months = List( "jan", "feb", "mar", "apr", "may", "jun", "jul", "aug", "sep", "oct", "nov", "dec") def is_month(s: String): Boolean = months.contains(s.toLowerCase) private val commands = List("preamble", "string") def is_command(s: String): Boolean = commands.contains(s.toLowerCase) sealed case class Entry( kind: String, required: List[String], optional_crossref: List[String], optional_other: List[String] ) { val optional_standard: List[String] = List("url", "doi", "ee") def is_required(s: String): Boolean = required.contains(s.toLowerCase) def is_optional(s: String): Boolean = optional_crossref.contains(s.toLowerCase) || optional_other.contains(s.toLowerCase) || optional_standard.contains(s.toLowerCase) def fields: List[String] = required ::: optional_crossref ::: optional_other ::: optional_standard def template: String = "@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n" } val known_entries: List[Entry] = List( Entry("Article", List("author", "title"), List("journal", "year"), List("volume", "number", "pages", "month", "note")), Entry("InProceedings", List("author", "title"), List("booktitle", "year"), List("editor", "volume", "number", "series", "pages", "month", "address", "organization", "publisher", "note")), Entry("InCollection", List("author", "title", "booktitle"), List("publisher", "year"), List("editor", "volume", "number", "series", "type", "chapter", "pages", "edition", "month", "address", "note")), Entry("InBook", List("author", "editor", "title", "chapter"), List("publisher", "year"), List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")), Entry("Proceedings", List("title", "year"), List(), List("booktitle", "editor", "volume", "number", "series", "address", "month", "organization", "publisher", "note")), Entry("Book", List("author", "editor", "title"), List("publisher", "year"), List("volume", "number", "series", "address", "edition", "month", "note")), Entry("Booklet", List("title"), List(), List("author", "howpublished", "address", "month", "year", "note")), Entry("PhdThesis", List("author", "title", "school", "year"), List(), List("type", "address", "month", "note")), Entry("MastersThesis", List("author", "title", "school", "year"), List(), List("type", "address", "month", "note")), Entry("TechReport", List("author", "title", "institution", "year"), List(), List("type", "number", "address", "month", "note")), Entry("Manual", List("title"), List(), List("author", "organization", "address", "edition", "month", "year", "note")), Entry("Unpublished", List("author", "title", "note"), List(), List("month", "year")), Entry("Misc", List(), List(), List("author", "title", "howpublished", "month", "year", "note"))) def get_entry(kind: String): Option[Entry] = known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase) def is_entry(kind: String): Boolean = get_entry(kind).isDefined /** tokens and chunks **/ object Token { object Kind extends Enumeration { val COMMAND = Value("command") val ENTRY = Value("entry") val KEYWORD = Value("keyword") val NAT = Value("natural number") val STRING = Value("string") val NAME = Value("name") val IDENT = Value("identifier") val SPACE = Value("white space") val COMMENT = Value("ignored text") val ERROR = Value("bad input") } } sealed case class Token(kind: Token.Kind.Value, source: String) { def is_kind: Boolean = kind == Token.Kind.COMMAND || kind == Token.Kind.ENTRY || kind == Token.Kind.IDENT def is_name: Boolean = kind == Token.Kind.NAME || kind == Token.Kind.IDENT def is_ignored: Boolean = kind == Token.Kind.SPACE || kind == Token.Kind.COMMENT def is_malformed: Boolean = kind == Token.Kind.ERROR def is_open: Boolean = kind == Token.Kind.KEYWORD && (source == "{" || source == "(") } case class Chunk(kind: String, tokens: List[Token]) { val source: String = tokens.map(_.source).mkString private val content: Option[List[Token]] = tokens match { case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty => (body.init.filterNot(_.is_ignored), body.last) match { case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}")) if tok.is_kind => Some(toks) case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")")) if tok.is_kind => Some(toks) case _ => None } case _ => None } def name: String = content match { case Some(tok :: _) if tok.is_name => tok.source case _ => "" } def heading_length: Int = if (name == "") 1 else { tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length } } def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored) def is_malformed: Boolean = tokens.exists(_.is_malformed) def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined } /** parsing **/ // context of partial line-oriented scans abstract class Line_Context case object Ignored extends Line_Context case object At extends Line_Context case class Item_Start(kind: String) extends Line_Context case class Item_Open(kind: String, end: String) extends Line_Context case class Item(kind: String, end: String, delim: Delimited) extends Line_Context case class Delimited(quoted: Boolean, depth: Int) val Closed: Delimited = Delimited(false, 0) private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source) private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source) // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web // module @. object Parsers extends RegexParsers { /* white space and comments */ override val whiteSpace = "".r private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE) private val spaces = rep(space) /* ignored text */ private val ignored: Parser[Chunk] = rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ { case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) } private def ignored_line: Parser[(Chunk, Line_Context)] = ignored ^^ { case a => (a, Ignored) } /* delimited string: outermost "..." or {...} and body with balanced {...} */ // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] = new Parser[(String, Delimited)] { require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0, "bad delimiter depth") def apply(in: Input): ParseResult[(String, Delimited)] = { val start = in.offset val end = in.source.length var i = start var q = delim.quoted var d = delim.depth var finished = false while (!finished && i < end) { val c = in.source.charAt(i) if (c == '"' && d == 0) { i += 1; d = 1; q = true } else if (c == '"' && d == 1 && q) { i += 1; d = 0; q = false; finished = true } else if (c == '{') { i += 1; d += 1 } else if (c == '}') { if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true } else {i = start; finished = true } } else if (d > 0) i += 1 else finished = true } if (i == start) Failure("bad input", in) else { val s = in.source.subSequence(start, i).toString Success((s, Delimited(q, d)), in.drop(i - start)) } } }.named("delimited_depth") private def delimited: Parser[Token] = delimited_depth(Closed) ^? { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) } private def recover_delimited: Parser[Token] = """["{][^@]*""".r ^^ token(Token.Kind.ERROR) def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] = delimited_depth(ctxt.delim) ^^ { case (s, delim1) => (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } | recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) } /* other tokens */ private val at = "@" ^^ keyword private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT) private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME) private val identifier = """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r private val ident = identifier ^^ token(Token.Kind.IDENT) val other_token: Parser[Token] = "[=#,]".r ^^ keyword | (nat | (ident | space)) /* body */ private val body = delimited | (recover_delimited | other_token) private def body_line(ctxt: Item) = if (ctxt.delim.depth > 0) delimited_line(ctxt) else delimited_line(ctxt) | other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } | ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) } /* items: command or entry */ private val item_kind = identifier ^^ { case a => val kind = if (is_command(a)) Token.Kind.COMMAND else if (is_entry(a)) Token.Kind.ENTRY else Token.Kind.IDENT Token(kind, a) } private val item_begin = "{" ^^ { case a => ("}", keyword(a)) } | "(" ^^ { case a => (")", keyword(a)) } private def item_name(kind: String) = kind.toLowerCase match { case "preamble" => failure("") case "string" => identifier ^^ token(Token.Kind.NAME) case _ => name } private val item_start = at ~ spaces ~ item_kind ~ spaces ^^ { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) } private val item: Parser[Chunk] = (item_start ~ item_begin ~ spaces) into { case (kind, a) ~ ((end, b)) ~ c => opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ { case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } } private val recover_item: Parser[Chunk] = at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) } /* chunks */ val chunk: Parser[Chunk] = ignored | (item | recover_item) def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = { ctxt match { case Ignored => ignored_line | at ^^ { case a => (Chunk("", List(a)), At) } case At => space ^^ { case a => (Chunk("", List(a)), ctxt) } | item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } | recover_item ^^ { case a => (a, Ignored) } | ignored_line case Item_Start(kind) => space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } | recover_item ^^ { case a => (a, Ignored) } | ignored_line case Item_Open(kind, end) => space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } | body_line(Item(kind, end, Closed)) | ignored_line case item_ctxt: Item => body_line(item_ctxt) | ignored_line case _ => failure("") } } } /* parse */ def parse(input: CharSequence): List[Chunk] = Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match { case Parsers.Success(result, _) => result case _ => error("Unexpected failure to parse input:\n" + input.toString) } def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = { var in: Reader[Char] = Scan.char_reader(input) val chunks = new mutable.ListBuffer[Chunk] var ctxt = context while (!in.atEnd) { val result = Parsers.parse(Parsers.chunk_line(ctxt), in) (result : @unchecked) match { case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest case Parsers.NoSuccess(_, rest) => error("Unepected failure to parse input:\n" + rest.source.toString) } } (chunks.toList, ctxt) } /** HTML output **/ private val output_styles = List( "" -> "html-n", "plain" -> "html-n", "alpha" -> "html-a", "named" -> "html-n", "paragraph" -> "html-n", "unsort" -> "html-u", "unsortlist" -> "html-u") def html_output(bib: List[Path], title: String = "Bibliography", body: Boolean = false, citations: List[String] = List("*"), style: String = "", chronological: Boolean = false ): String = { Isabelle_System.with_tmp_dir("bibtex") { tmp_dir => /* database files */ val bib_files = bib.map(_.drop_ext) val bib_names = { val names0 = bib_files.map(_.file_name) if (Library.duplicates(names0).isEmpty) names0 else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name }) } for ((a, b) <- bib_files zip bib_names) { Isabelle_System.copy_file(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib")) } /* style file */ val bst = output_styles.toMap.get(style) match { case Some(base) => base + (if (chronological) "c" else "") + ".bst" case None => error("Bad style for bibtex HTML output: " + quote(style) + "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")") } Isabelle_System.copy_file(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir) /* result */ val in_file = Path.explode("bib.aux") val out_file = Path.explode("bib.html") File.write(tmp_dir + in_file, bib_names.mkString("\\bibdata{", ",", "}\n") + citations.map(cite => "\\citation{" + cite + "}\n").mkString) Isabelle_System.bash( "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" + " -u -s " + Bash.string(proper_string(style) getOrElse "empty") + (if (chronological) " -c" else "") + (if (title != "") " -h " + Bash.string(title) + " " else "") + " " + File.bash_path(in_file) + " " + File.bash_path(out_file), cwd = tmp_dir.file).check val html = File.read(tmp_dir + out_file) if (body) { cat_lines( split_lines(html). dropWhile(line => !line.startsWith("), dest_funT, (--->), aconv, list_comb, strip_comb, head_of ) where import Isabelle.Library import qualified Isabelle.Name as Name import Isabelle.Name (Name) infixr 5 --> infixr ---> {- types and terms -} type Indexname = (Name, Int) type Sort = [Name] data Typ = Type (Name, [Typ]) | TFree (Name, Sort) | TVar (Indexname, Sort) deriving (Show, Eq, Ord) data Term = Const (Name, [Typ]) | Free (Name, Typ) | Var (Indexname, Typ) | Bound Int | Abs (Name, Typ, Term) | App (Term, Term) deriving (Show, Eq, Ord) {- free and bound variables -} type Free = (Name, Typ) lambda :: Free -> Term -> Term lambda (name, typ) body = Abs (name, typ, abstract 0 body) where abstract lev (Free (x, ty)) | name == x && typ == ty = Bound lev abstract lev (Abs (a, ty, t)) = Abs (a, ty, abstract (lev + 1) t) abstract lev (App (t, u)) = App (abstract lev t, abstract lev u) abstract _ t = t declare_frees :: Term -> Name.Context -> Name.Context declare_frees (Free (x, _)) = Name.declare x declare_frees (Abs (_, _, b)) = declare_frees b declare_frees (App (t, u)) = declare_frees t #> declare_frees u declare_frees _ = id incr_boundvars :: Int -> Term -> Term incr_boundvars inc = if inc == 0 then id else incr 0 where incr lev (Bound i) = if i >= lev then Bound (i + inc) else Bound i incr lev (Abs (a, ty, b)) = Abs (a, ty, incr (lev + 1) b) incr lev (App (t, u)) = App (incr lev t, incr lev u) incr _ t = t subst_bound :: Term -> Term -> Term subst_bound arg = subst 0 where subst lev (Bound i) = if i < lev then Bound i else if i == lev then incr_boundvars lev arg else Bound (i - 1) subst lev (Abs (a, ty, b)) = Abs (a, ty, subst (lev + 1) b) subst lev (App (t, u)) = App (subst lev t, subst lev u) subst _ t = t dest_lambda :: Name.Context -> Term -> Maybe (Free, Term) dest_lambda names (Abs (x, ty, b)) = let (x', _) = Name.variant x (declare_frees b names) v = (x', ty) in Just (v, subst_bound (Free v) b) dest_lambda _ _ = Nothing strip_lambda :: Name.Context -> Term -> ([Free], Term) strip_lambda names tm = case dest_lambda names tm of Just (v, t) -> let (vs, t') = strip_lambda names t' in (v : vs, t') Nothing -> ([], tm) {- type and term operators -} type_op0 :: Name -> (Typ, Typ -> Bool) type_op0 name = (mk, is) where mk = Type (name, []) is (Type (c, _)) = c == name is _ = False type_op1 :: Name -> (Typ -> Typ, Typ -> Maybe Typ) type_op1 name = (mk, dest) where mk ty = Type (name, [ty]) dest (Type (c, [ty])) | c == name = Just ty dest _ = Nothing type_op2 :: Name -> (Typ -> Typ -> Typ, Typ -> Maybe (Typ, Typ)) type_op2 name = (mk, dest) where mk ty1 ty2 = Type (name, [ty1, ty2]) dest (Type (c, [ty1, ty2])) | c == name = Just (ty1, ty2) dest _ = Nothing op0 :: Name -> (Term, Term -> Bool) op0 name = (mk, is) where mk = Const (name, []) is (Const (c, _)) = c == name is _ = False op1 :: Name -> (Term -> Term, Term -> Maybe Term) op1 name = (mk, dest) where mk t = App (Const (name, []), t) dest (App (Const (c, _), t)) | c == name = Just t dest _ = Nothing op2 :: Name -> (Term -> Term -> Term, Term -> Maybe (Term, Term)) op2 name = (mk, dest) where mk t u = App (App (Const (name, []), t), u) dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u) dest _ = Nothing typed_op0 :: Name -> (Typ -> Term, Term -> Maybe Typ) typed_op0 name = (mk, dest) where mk ty = Const (name, [ty]) dest (Const (c, [ty])) | c == name = Just ty dest _ = Nothing typed_op1 :: Name -> (Typ -> Term -> Term, Term -> Maybe (Typ, Term)) typed_op1 name = (mk, dest) where mk ty t = App (Const (name, [ty]), t) dest (App (Const (c, [ty]), t)) | c == name = Just (ty, t) dest _ = Nothing typed_op2 :: Name -> (Typ -> Term -> Term -> Term, Term -> Maybe (Typ, Term, Term)) typed_op2 name = (mk, dest) where mk ty t u = App (App (Const (name, [ty]), t), u) dest (App (App (Const (c, [ty]), t), u)) | c == name = Just (ty, t, u) dest _ = Nothing binder :: Name -> (Free -> Term -> Term, Name.Context -> Term -> Maybe (Free, Term)) binder name = (mk, dest) where mk (a, ty) b = App (Const (name, [ty]), lambda (a, ty) b) dest names (App (Const (c, _), t)) | c == name = dest_lambda names t dest _ _ = Nothing {- type operations -} dummyS :: Sort dummyS = [""] dummyT :: Typ; is_dummyT :: Typ -> Bool (dummyT, is_dummyT) = type_op0 \\<^type_name>\dummy\\ propT :: Typ; is_propT :: Typ -> Bool (propT, is_propT) = type_op0 \\<^type_name>\prop\\ (-->) :: Typ -> Typ -> Typ; dest_funT :: Typ -> Maybe (Typ, Typ) ((-->), dest_funT) = type_op2 \\<^type_name>\fun\\ (--->) :: [Typ] -> Typ -> Typ [] ---> b = b (a : as) ---> b = a --> (as ---> b) {- term operations -} aconv :: Term -> Term -> Bool aconv (App (t1, u1)) (App (t2, u2)) = aconv t1 t2 && aconv u1 u2 aconv (Abs (_, ty1, t1)) (Abs (_, ty2, t2)) = aconv t1 t2 && ty1 == ty2 aconv a1 a2 = a1 == a2 list_comb :: Term -> [Term] -> Term list_comb f [] = f list_comb f (t : ts) = list_comb (App (f, t)) ts strip_comb :: Term -> (Term, [Term]) strip_comb tm = strip (tm, []) where strip (App (f, t), ts) = strip (f, t : ts) strip x = x head_of :: Term -> Term head_of (App (f, _)) = head_of f head_of u = u \ generate_file "Isabelle/Pure.hs" = \ {- Title: Isabelle/Term.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Support for Isabelle/Pure logic. See \<^file>\$ISABELLE_HOME/src/Pure/logic.ML\. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Pure ( mk_forall_op, dest_forall_op, mk_forall, dest_forall, mk_equals, dest_equals, mk_implies, dest_implies ) where import qualified Isabelle.Name as Name import Isabelle.Term mk_forall_op :: Typ -> Term -> Term; dest_forall_op :: Term -> Maybe (Typ, Term) (mk_forall_op, dest_forall_op) = typed_op1 \\<^const_name>\Pure.all\\ mk_forall :: Free -> Term -> Term; dest_forall :: Name.Context -> Term -> Maybe (Free, Term) (mk_forall, dest_forall) = binder \\<^const_name>\Pure.all\\ mk_equals :: Typ -> Term -> Term -> Term; dest_equals :: Term -> Maybe (Typ, Term, Term) (mk_equals, dest_equals) = typed_op2 \\<^const_name>\Pure.eq\\ mk_implies :: Term -> Term -> Term; dest_implies :: Term -> Maybe (Term, Term) (mk_implies, dest_implies) = op2 \\<^const_name>\Pure.imp\\ \ generate_file "Isabelle/HOL.hs" = \ {- Title: Isabelle/Term.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Support for Isabelle/HOL logic. See \<^file>\$ISABELLE_HOME/src/HOL/Tools/hologic.ML\. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.HOL ( boolT, is_boolT, mk_trueprop, dest_trueprop, mk_setT, dest_setT, mk_mem, dest_mem, mk_eq, dest_eq, true, is_true, false, is_false, mk_not, dest_not, mk_conj, dest_conj, mk_disj, dest_disj, mk_imp, dest_imp, mk_iff, dest_iff, mk_all_op, dest_all_op, mk_ex_op, dest_ex_op, mk_all, dest_all, mk_ex, dest_ex, mk_undefined, dest_undefined ) where import qualified Isabelle.Name as Name import Isabelle.Term boolT :: Typ; is_boolT :: Typ -> Bool (boolT, is_boolT) = type_op0 \\<^type_name>\bool\\ mk_trueprop :: Term -> Term; dest_trueprop :: Term -> Maybe Term (mk_trueprop, dest_trueprop) = op1 \\<^const_name>\Trueprop\\ mk_setT :: Typ -> Typ; dest_setT :: Typ -> Maybe Typ (mk_setT, dest_setT) = type_op1 \\<^type_name>\set\\ mk_mem :: Typ -> Term -> Term -> Term; dest_mem :: Term -> Maybe (Typ, Term, Term) (mk_mem, dest_mem) = typed_op2 \\<^const_name>\Set.member\\ mk_eq :: Typ -> Term -> Term -> Term; dest_eq :: Term -> Maybe (Typ, Term, Term) (mk_eq, dest_eq) = typed_op2 \\<^const_name>\HOL.eq\\ true :: Term; is_true :: Term -> Bool (true, is_true) = op0 \\<^const_name>\True\\ false :: Term; is_false :: Term -> Bool (false, is_false) = op0 \\<^const_name>\False\\ mk_not :: Term -> Term; dest_not :: Term -> Maybe Term (mk_not, dest_not) = op1 \\<^const_name>\Not\\ mk_conj :: Term -> Term -> Term; dest_conj :: Term -> Maybe (Term, Term) (mk_conj, dest_conj) = op2 \\<^const_name>\conj\\ mk_disj :: Term -> Term -> Term; dest_disj :: Term -> Maybe (Term, Term) (mk_disj, dest_disj) = op2 \\<^const_name>\disj\\ mk_imp :: Term -> Term -> Term; dest_imp :: Term -> Maybe (Term, Term) (mk_imp, dest_imp) = op2 \\<^const_name>\implies\\ mk_iff :: Term -> Term -> Term mk_iff = mk_eq boolT dest_iff :: Term -> Maybe (Term, Term) dest_iff tm = case dest_eq tm of Just (ty, t, u) | ty == boolT -> Just (t, u) _ -> Nothing mk_all_op :: Typ -> Term -> Term; dest_all_op :: Term -> Maybe (Typ, Term) (mk_all_op, dest_all_op) = typed_op1 \\<^const_name>\All\\ mk_ex_op :: Typ -> Term -> Term; dest_ex_op :: Term -> Maybe (Typ, Term) (mk_ex_op, dest_ex_op) = typed_op1 \\<^const_name>\Ex\\ mk_all :: Free -> Term -> Term; dest_all :: Name.Context -> Term -> Maybe (Free, Term) (mk_all, dest_all) = binder \\<^const_name>\All\\ mk_ex :: Free -> Term -> Term; dest_ex :: Name.Context -> Term -> Maybe (Free, Term) (mk_ex, dest_ex) = binder \\<^const_name>\Ex\\ mk_undefined :: Typ -> Term; dest_undefined :: Term -> Maybe Typ (mk_undefined, dest_undefined) = typed_op0 \\<^const_name>\undefined\\ \ generate_file "Isabelle/Term_XML/Encode.hs" = \ {- Title: Isabelle/Term_XML/Encode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) XML data representation of lambda terms. See \<^file>\$ISABELLE_HOME/src/Pure/term_xml.ML\. -} {-# LANGUAGE LambdaCase #-} module Isabelle.Term_XML.Encode (indexname, sort, typ, typ_body, term) where import Isabelle.Library import Isabelle.XML.Encode import Isabelle.Term indexname :: P Indexname indexname (a, b) = if b == 0 then [a] else [a, int_atom b] sort :: T Sort sort = list string typ :: T Typ typ ty = ty |> variant [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing }, \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing }, \case { TVar (a, b) -> Just (indexname a, sort b); _ -> Nothing }] typ_body :: T Typ typ_body ty = if is_dummyT ty then [] else typ ty term :: T Term term t = t |> variant [\case { Const (a, b) -> Just ([a], list typ b); _ -> Nothing }, \case { Free (a, b) -> Just ([a], typ_body b); _ -> Nothing }, \case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing }, \case { Bound a -> Just ([], int a); _ -> Nothing }, \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing }, \case { App a -> Just ([], pair term term a); _ -> Nothing }] \ generate_file "Isabelle/Term_XML/Decode.hs" = \ {- Title: Isabelle/Term_XML/Decode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) XML data representation of lambda terms. See \<^file>\$ISABELLE_HOME/src/Pure/term_xml.ML\. -} {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} module Isabelle.Term_XML.Decode (indexname, sort, typ, typ_body, term) where import Isabelle.Library import Isabelle.XML.Decode import Isabelle.Term indexname :: P Indexname indexname [a] = (a, 0) indexname [a, b] = (a, int_atom b) sort :: T Sort sort = list string typ :: T Typ typ ty = ty |> variant [\([a], b) -> Type (a, list typ b), \([a], b) -> TFree (a, sort b), \(a, b) -> TVar (indexname a, sort b)] typ_body :: T Typ typ_body [] = dummyT typ_body body = typ body term :: T Term term t = t |> variant [\([a], b) -> Const (a, list typ b), \([a], b) -> Free (a, typ_body b), \(a, b) -> Var (indexname a, typ_body b), \([], a) -> Bound (int a), \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d), \([], a) -> App (pair term term a)] \ generate_file "Isabelle/XML/Classes.hs" = \ {- generated by Isabelle -} {- Title: Isabelle/XML/Classes.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Type classes for XML data representation. -} {-# LANGUAGE FlexibleInstances #-} module Isabelle.XML.Classes (Encode_Atom(..), Decode_Atom(..), Encode (..), Decode (..)) where import qualified Isabelle.XML as XML import qualified Isabelle.XML.Encode as Encode import qualified Isabelle.XML.Decode as Decode import qualified Isabelle.Term_XML.Encode as Encode import qualified Isabelle.Term_XML.Decode as Decode import qualified Isabelle.Properties as Properties import Isabelle.Bytes (Bytes) import Isabelle.Term (Typ, Term) class Encode_Atom a where encode_atom :: Encode.A a class Decode_Atom a where decode_atom :: Decode.A a instance Encode_Atom Int where encode_atom = Encode.int_atom instance Decode_Atom Int where decode_atom = Decode.int_atom instance Encode_Atom Bool where encode_atom = Encode.bool_atom instance Decode_Atom Bool where decode_atom = Decode.bool_atom instance Encode_Atom () where encode_atom = Encode.unit_atom instance Decode_Atom () where decode_atom = Decode.unit_atom class Encode a where encode :: Encode.T a class Decode a where decode :: Decode.T a instance Encode Bytes where encode = Encode.string instance Decode Bytes where decode = Decode.string instance Encode Int where encode = Encode.int instance Decode Int where decode = Decode.int instance Encode Bool where encode = Encode.bool instance Decode Bool where decode = Decode.bool instance Encode () where encode = Encode.unit instance Decode () where decode = Decode.unit instance (Encode a, Encode b) => Encode (a, b) where encode = Encode.pair encode encode instance (Decode a, Decode b) => Decode (a, b) where decode = Decode.pair decode decode instance (Encode a, Encode b, Encode c) => Encode (a, b, c) where encode = Encode.triple encode encode encode instance (Decode a, Decode b, Decode c) => Decode (a, b, c) where decode = Decode.triple decode decode decode instance Encode a => Encode [a] where encode = Encode.list encode instance Decode a => Decode [a] where decode = Decode.list decode instance Encode a => Encode (Maybe a) where encode = Encode.option encode instance Decode a => Decode (Maybe a) where decode = Decode.option decode instance Encode XML.Tree where encode = Encode.tree instance Decode XML.Tree where decode = Decode.tree instance Encode Properties.T where encode = Encode.properties instance Decode Properties.T where decode = Decode.properties instance Encode Typ where encode = Encode.typ instance Decode Typ where decode = Decode.typ instance Encode Term where encode = Encode.term instance Decode Term where decode = Decode.term \ generate_file "Isabelle/UUID.hs" = \ {- Title: Isabelle/UUID.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Universally unique identifiers. See \<^file>\$ISABELLE_HOME/src/Pure/General/uuid.scala\. -} module Isabelle.UUID (T, random, print, parse) where import Prelude hiding (print) import Data.UUID (UUID) import qualified Data.UUID as UUID import Data.UUID.V4 (nextRandom) import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) type T = UUID random :: IO T random = nextRandom print :: T -> Bytes print = Bytes.make . UUID.toASCIIBytes parse :: Bytes -> Maybe T parse = UUID.fromASCIIBytes . Bytes.unmake \ generate_file "Isabelle/Byte_Message.hs" = \ {- Title: Isabelle/Byte_Message.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Byte-oriented messages. See \<^file>\$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\ and \<^file>\$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\. -} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} module Isabelle.Byte_Message ( write, write_line, read, read_block, read_line, make_message, write_message, read_message, exchange_message, exchange_message0, make_line_message, write_line_message, read_line_message, read_yxml, write_yxml ) where import Prelude hiding (read) import Data.Maybe import qualified Data.ByteString as ByteString import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import qualified Isabelle.Symbol as Symbol import qualified Isabelle.UTF8 as UTF8 import qualified Isabelle.XML as XML import qualified Isabelle.YXML as YXML import Network.Socket (Socket) import qualified Network.Socket.ByteString as Socket import Isabelle.Library import qualified Isabelle.Value as Value {- output operations -} write :: Socket -> [Bytes] -> IO () write socket = Socket.sendMany socket . map Bytes.unmake write_line :: Socket -> Bytes -> IO () write_line socket s = write socket [s, "\n"] {- input operations -} read :: Socket -> Int -> IO Bytes read socket n = read_body 0 [] where result = Bytes.concat . reverse read_body len ss = if len >= n then return (result ss) else (do s <- Socket.recv socket (min (n - len) 8192) case ByteString.length s of 0 -> return (result ss) m -> read_body (len + m) (Bytes.make s : ss)) read_block :: Socket -> Int -> IO (Maybe Bytes, Int) read_block socket n = do msg <- read socket n let len = Bytes.length msg return (if len == n then Just msg else Nothing, len) read_line :: Socket -> IO (Maybe Bytes) read_line socket = read_body [] where result = trim_line . Bytes.pack . reverse read_body bs = do s <- Socket.recv socket 1 case ByteString.length s of 0 -> return (if null bs then Nothing else Just (result bs)) 1 -> case ByteString.head s of 10 -> return (Just (result bs)) b -> read_body (b : bs) {- messages with multiple chunks (arbitrary content) -} make_header :: [Int] -> [Bytes] make_header ns = [space_implode "," (map Value.print_int ns), "\n"] make_message :: [Bytes] -> [Bytes] make_message chunks = make_header (map Bytes.length chunks) <> chunks write_message :: Socket -> [Bytes] -> IO () write_message socket = write socket . make_message parse_header :: Bytes -> [Int] parse_header line = let res = map Value.parse_nat (space_explode ',' line) in if all isJust res then map fromJust res else error ("Malformed message header: " <> quote (UTF8.decode line)) read_chunk :: Socket -> Int -> IO Bytes read_chunk socket n = do res <- read_block socket n return $ case res of (Just chunk, _) -> chunk (Nothing, len) -> error ("Malformed message chunk: unexpected EOF after " <> show len <> " of " <> show n <> " bytes") read_message :: Socket -> IO (Maybe [Bytes]) read_message socket = do res <- read_line socket case res of Just line -> Just <$> mapM (read_chunk socket) (parse_header line) Nothing -> return Nothing exchange_message :: Socket -> [Bytes] -> IO (Maybe [Bytes]) exchange_message socket msg = do write_message socket msg read_message socket exchange_message0 :: Socket -> [Bytes] -> IO () exchange_message0 socket msg = do _ <- exchange_message socket msg return () -- hybrid messages: line or length+block (with content restriction) is_length :: Bytes -> Bool is_length msg = not (Bytes.null msg) && Bytes.all_char (\c -> '0' <= c && c <= '9') msg is_terminated :: Bytes -> Bool is_terminated msg = not (Bytes.null msg) && Symbol.is_ascii_line_terminator (Bytes.char $ Bytes.last msg) make_line_message :: Bytes -> [Bytes] make_line_message msg = let n = Bytes.length msg in if is_length msg || is_terminated msg then error ("Bad content for line message:\n" <> take 100 (UTF8.decode msg)) else (if n > 100 || Bytes.any_char (== '\n') msg then make_header [n + 1] else []) <> [msg, "\n"] write_line_message :: Socket -> Bytes -> IO () write_line_message socket = write socket . make_line_message read_line_message :: Socket -> IO (Maybe Bytes) read_line_message socket = do opt_line <- read_line socket case opt_line of Nothing -> return Nothing Just line -> case Value.parse_nat line of Nothing -> return $ Just line Just n -> fmap trim_line . fst <$> read_block socket n read_yxml :: Socket -> IO (Maybe XML.Body) read_yxml socket = do res <- read_line_message socket return (YXML.parse_body <$> res) write_yxml :: Socket -> XML.Body -> IO () write_yxml socket body = write_line_message socket (YXML.string_of_body body) \ generate_file "Isabelle/Isabelle_Thread.hs" = \ {- Title: Isabelle/Isabelle_Thread.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Isabelle-specific thread management. See \<^file>\$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.ML\ and \<^file>\$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.scala\. -} {-# LANGUAGE NamedFieldPuns #-} module Isabelle.Isabelle_Thread ( ThreadId, Result, find_id, properties, change_properties, add_resource, del_resource, bracket_resource, is_stopped, expose_stopped, stop, my_uuid, stop_uuid, Fork, fork_finally, fork) where import Data.Unique import Data.IORef import System.IO.Unsafe import qualified Data.List as List import Control.Monad (when, forM_) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Control.Exception as Exception import Control.Concurrent (ThreadId) import qualified Control.Concurrent as Concurrent import Control.Concurrent.Thread (Result) import qualified Control.Concurrent.Thread as Thread import qualified Isabelle.UUID as UUID import qualified Isabelle.Properties as Properties {- thread info -} type Resources = Map Unique (IO ()) data Info = Info {uuid :: UUID.T, props :: Properties.T, stopped :: Bool, resources :: Resources} type Infos = Map ThreadId Info lookup_info :: Infos -> ThreadId -> Maybe Info lookup_info infos id = Map.lookup id infos init_info :: ThreadId -> UUID.T -> Infos -> (Infos, ()) init_info id uuid infos = (Map.insert id (Info uuid [] False Map.empty) infos, ()) {- global state -} {-# NOINLINE global_state #-} global_state :: IORef Infos global_state = unsafePerformIO (newIORef Map.empty) find_id :: UUID.T -> IO (Maybe ThreadId) find_id uuid = do state <- readIORef global_state return $ fst <$> List.find (\(_, Info{uuid = uuid'}) -> uuid == uuid') (Map.assocs state) get_info :: ThreadId -> IO (Maybe Info) get_info id = do state <- readIORef global_state return $ lookup_info state id map_info :: ThreadId -> (Info -> Info) -> IO (Maybe Info) map_info id f = atomicModifyIORef' global_state (\infos -> case lookup_info infos id of Nothing -> (infos, Nothing) Just info -> let info' = f info in (Map.insert id info' infos, Just info')) delete_info :: ThreadId -> IO () delete_info id = atomicModifyIORef' global_state (\infos -> (Map.delete id infos, ())) {- thread properties -} my_info :: IO (Maybe Info) my_info = do id <- Concurrent.myThreadId get_info id properties :: IO Properties.T properties = maybe [] props <$> my_info change_properties :: (Properties.T -> Properties.T) -> IO () change_properties f = do id <- Concurrent.myThreadId map_info id (\info -> info {props = f (props info)}) return () {- managed resources -} add_resource :: IO () -> IO Unique add_resource resource = do id <- Concurrent.myThreadId u <- newUnique map_info id (\info -> info {resources = Map.insert u resource (resources info)}) return u del_resource :: Unique -> IO () del_resource u = do id <- Concurrent.myThreadId map_info id (\info -> info {resources = Map.delete u (resources info)}) return () bracket_resource :: IO () -> IO a -> IO a bracket_resource resource body = Exception.bracket (add_resource resource) del_resource (const body) {- stop -} is_stopped :: IO Bool is_stopped = maybe False stopped <$> my_info expose_stopped :: IO () expose_stopped = do stopped <- is_stopped when stopped $ throw ThreadKilled stop :: ThreadId -> IO () stop id = do info <- map_info id (\info -> info {stopped = True}) let ops = case info of Nothing -> []; Just Info{resources} -> map snd (Map.toDescList resources) sequence_ ops {- UUID -} my_uuid :: IO (Maybe UUID.T) my_uuid = fmap uuid <$> my_info stop_uuid :: UUID.T -> IO () stop_uuid uuid = do id <- find_id uuid forM_ id stop {- fork -} type Fork a = (ThreadId, UUID.T, IO (Result a)) fork_finally :: IO a -> (Either SomeException a -> IO b) -> IO (Fork b) fork_finally body finally = do uuid <- UUID.random (id, result) <- Exception.mask (\restore -> Thread.forkIO (Exception.try (do id <- Concurrent.myThreadId atomicModifyIORef' global_state (init_info id uuid) restore body) >>= (\res -> do id <- Concurrent.myThreadId; delete_info id; finally res))) return (id, uuid, result) fork :: IO a -> IO (Fork a) fork body = fork_finally body Thread.result \ generate_file "Isabelle/Server.hs" = \ {- Title: Isabelle/Server.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) TCP server on localhost. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Server ( localhost_name, localhost_prefix, localhost, publish_text, publish_stdout, server, connection ) where import Control.Monad (forever, when) import qualified Control.Exception as Exception import Network.Socket (Socket) import qualified Network.Socket as Socket import qualified System.IO as IO import qualified Data.ByteString.Char8 as Char8 import Isabelle.Library import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import qualified Isabelle.UUID as UUID import qualified Isabelle.Byte_Message as Byte_Message import qualified Isabelle.Isabelle_Thread as Isabelle_Thread {- server address -} localhost_name :: Bytes localhost_name = "127.0.0.1" localhost_prefix :: Bytes localhost_prefix = localhost_name <> ":" localhost :: Socket.HostAddress localhost = Socket.tupleToHostAddress (127, 0, 0, 1) publish_text :: Bytes -> Bytes -> UUID.T -> Bytes publish_text name address password = "server " <> quote name <> " = " <> address <> " (password " <> quote (show_bytes password) <> ")" publish_stdout :: Bytes -> Bytes -> UUID.T -> IO () publish_stdout name address password = Char8.putStrLn (Bytes.unmake $ publish_text name address password) {- server -} server :: (Bytes -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO () server publish handle = Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop) where open :: IO (Socket, Bytes) open = do server_socket <- Socket.socket Socket.AF_INET Socket.Stream Socket.defaultProtocol Socket.bind server_socket (Socket.SockAddrInet 0 localhost) Socket.listen server_socket 50 port <- Socket.socketPort server_socket let address = localhost_name <> ":" <> show_bytes port password <- UUID.random publish address password return (server_socket, UUID.print password) loop :: Socket -> Bytes -> IO () loop server_socket password = forever $ do (connection, _) <- Socket.accept server_socket Isabelle_Thread.fork_finally (do line <- Byte_Message.read_line connection when (line == Just password) $ handle connection) (\finally -> do Socket.close connection case finally of Left exn -> IO.hPutStrLn IO.stderr $ Exception.displayException exn Right () -> return ()) return () {- client connection -} connection :: String -> Bytes -> (Socket -> IO a) -> IO a connection port password client = Socket.withSocketsDo $ do addr <- resolve Exception.bracket (open addr) Socket.close body where resolve = do let hints = Socket.defaultHints { Socket.addrFlags = [Socket.AI_NUMERICHOST, Socket.AI_NUMERICSERV], Socket.addrSocketType = Socket.Stream } head <$> Socket.getAddrInfo (Just hints) (Just $ make_string localhost_name) (Just port) open addr = do socket <- Socket.socket (Socket.addrFamily addr) (Socket.addrSocketType addr) (Socket.addrProtocol addr) Socket.connect socket $ Socket.addrAddress addr return socket body socket = do Byte_Message.write_line socket password client socket \ generate_file "Isabelle/Time.hs" = \ {- Title: Isabelle/Time.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Time based on milliseconds. See \<^file>\~~/src/Pure/General/time.scala\ -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Time ( Time, seconds, minutes, ms, zero, is_zero, is_relevant, get_seconds, get_minutes, get_ms, message, now ) where import Text.Printf (printf) import Data.Time.Clock.POSIX (getPOSIXTime) import Isabelle.Bytes (Bytes) import Isabelle.Library newtype Time = Time Int instance Eq Time where Time a == Time b = a == b instance Ord Time where compare (Time a) (Time b) = compare a b instance Num Time where fromInteger = Time . fromInteger Time a + Time b = Time (a + b) Time a - Time b = Time (a - b) Time a * Time b = Time (a * b) abs (Time a) = Time (abs a) signum (Time a) = Time (signum a) seconds :: Double -> Time seconds s = Time (round (s * 1000.0)) minutes :: Double -> Time minutes m = Time (round (m * 60000.0)) ms :: Int -> Time ms = Time zero :: Time zero = ms 0 is_zero :: Time -> Bool is_zero (Time ms) = ms == 0 is_relevant :: Time -> Bool is_relevant (Time ms) = ms >= 1 get_seconds :: Time -> Double get_seconds (Time ms) = fromIntegral ms / 1000.0 get_minutes :: Time -> Double get_minutes (Time ms) = fromIntegral ms / 60000.0 get_ms :: Time -> Int get_ms (Time ms) = ms instance Show Time where show t = printf "%.3f" (get_seconds t) message :: Time -> Bytes message t = make_bytes (show t) <> "s" now :: IO Time now = do t <- getPOSIXTime return $ Time (round (realToFrac t * 1000.0 :: Double)) \ generate_file "Isabelle/Timing.hs" = \ {- Title: Isabelle/Timing.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Support for time measurement. See \<^file>\~~/src/Pure/General/timing.ML\ and \<^file>\~~/src/Pure/General/timing.scala\ -} module Isabelle.Timing ( Timing (..), zero, is_zero, is_relevant ) where import qualified Isabelle.Time as Time import Isabelle.Time (Time) data Timing = Timing {elapsed :: Time, cpu :: Time, gc :: Time} deriving (Show, Eq) zero :: Timing zero = Timing Time.zero Time.zero Time.zero is_zero :: Timing -> Bool is_zero t = Time.is_zero (elapsed t) && Time.is_zero (cpu t) && Time.is_zero (gc t) is_relevant :: Timing -> Bool is_relevant t = Time.is_relevant (elapsed t) || Time.is_relevant (cpu t) || Time.is_relevant (gc t) \ generate_file "Isabelle/Bash.hs" = \ {- Title: Isabelle/Bash.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Support for GNU bash. See \<^file>\$ISABELLE_HOME/src/Pure/System/bash.ML\ -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Bash ( string, strings, Params, get_script, get_input, get_cwd, get_putenv, get_redirect, get_timeout, get_description, script, input, cwd, putenv, redirect, timeout, description, server_run, server_kill, server_uuid, server_interrupt, server_failure, server_result ) where import Text.Printf (printf) import qualified Isabelle.Symbol as Symbol import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import qualified Isabelle.Time as Time import Isabelle.Time (Time) import Isabelle.Library {- concrete syntax -} string :: Bytes -> Bytes string str = if Bytes.null str then "\"\"" else str |> Bytes.unpack |> map trans |> Bytes.concat where trans b = case Bytes.char b of '\t' -> "$'\\t'" '\n' -> "$'\\n'" '\f' -> "$'\\f'" '\r' -> "$'\\r'" c -> if Symbol.is_ascii_letter c || Symbol.is_ascii_digit c || c `elem` ("+,-./:_" :: String) then Bytes.singleton b else if b < 32 || b >= 127 then make_bytes (printf "$'\\x%02x'" b :: String) else "\\" <> Bytes.singleton b strings :: [Bytes] -> Bytes strings = space_implode " " . map string {- server parameters -} data Params = Params { _script :: Bytes, _input :: Bytes, _cwd :: Maybe Bytes, _putenv :: [(Bytes, Bytes)], _redirect :: Bool, _timeout :: Time, _description :: Bytes} deriving (Show, Eq) get_script :: Params -> Bytes get_script = _script get_input :: Params -> Bytes get_input = _input get_cwd :: Params -> Maybe Bytes get_cwd = _cwd get_putenv :: Params -> [(Bytes, Bytes)] get_putenv = _putenv get_redirect :: Params -> Bool get_redirect = _redirect get_timeout :: Params -> Time get_timeout = _timeout get_description :: Params -> Bytes get_description = _description script :: Bytes -> Params script script = Params script "" Nothing [] False Time.zero "" input :: Bytes -> Params -> Params input input params = params { _input = input } cwd :: Bytes -> Params -> Params cwd cwd params = params { _cwd = Just cwd } putenv :: [(Bytes, Bytes)] -> Params -> Params putenv putenv params = params { _putenv = putenv } redirect :: Params -> Params redirect params = params { _redirect = True } timeout :: Time -> Params -> Params timeout timeout params = params { _timeout = timeout } description :: Bytes -> Params -> Params description description params = params { _description = description } {- server messages -} server_run, server_kill :: Bytes server_run = \Bash.server_run\; server_kill = \Bash.server_kill\; server_uuid, server_interrupt, server_failure, server_result :: Bytes server_uuid = \Bash.server_uuid\; server_interrupt = \Bash.server_interrupt\; server_failure = \Bash.server_failure\; server_result = \Bash.server_result\; \ generate_file "Isabelle/Process_Result.hs" = \ {- Title: Isabelle/Process_Result.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Result of system process. See \<^file>\~~/src/Pure/System/process_result.ML\ and \<^file>\~~/src/Pure/System/process_result.scala\ -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Process_Result ( ok_rc, error_rc, failure_rc, interrupt_rc , timeout_rc, T, make, rc, out_lines, err_lines, timing, timing_elapsed, out, err, ok, check ) where import Isabelle.Time (Time) import qualified Isabelle.Timing as Timing import Isabelle.Timing (Timing) import Isabelle.Bytes (Bytes) import Isabelle.Library ok_rc, error_rc, failure_rc, interrupt_rc , timeout_rc :: Int ok_rc = 0 error_rc = 1 failure_rc = 2 interrupt_rc = 130 timeout_rc = 142 data T = Process_Result { _rc :: Int, _out_lines :: [Bytes], _err_lines :: [Bytes], _timing :: Timing} deriving (Show, Eq) make :: Int -> [Bytes] -> [Bytes] -> Timing -> T make = Process_Result rc :: T -> Int rc = _rc out_lines :: T -> [Bytes] out_lines = _out_lines err_lines :: T -> [Bytes] err_lines = _err_lines timing :: T -> Timing timing = _timing timing_elapsed :: T -> Time timing_elapsed = Timing.elapsed . timing out :: T -> Bytes out = trim_line . cat_lines . out_lines err :: T -> Bytes err = trim_line . cat_lines . err_lines ok :: T -> Bool ok result = rc result == ok_rc check :: T -> T check result = if ok result then result else error (make_string $ err result) \ generate_file "Isabelle/Options.hs" = \ {- Title: Isabelle/Options.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) System options with external string representation. See \<^file>\~~/src/Pure/System/options.ML\ and \<^file>\~~/src/Pure/System/options.scala\ -} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE InstanceSigs #-} module Isabelle.Options ( boolT, intT, realT, stringT, unknownT, T, typ, bool, int, real, seconds, string, decode ) where import qualified Data.Map.Strict as Map import Data.Map.Strict (Map) import qualified Isabelle.Properties as Properties import Isabelle.Bytes (Bytes) import qualified Isabelle.Value as Value import qualified Isabelle.Time as Time import Isabelle.Time (Time) import Isabelle.Library import qualified Isabelle.XML.Decode as Decode import Isabelle.XML.Classes (Decode (..)) {- representation -} boolT :: Bytes boolT = "bool" intT :: Bytes intT = "int" realT :: Bytes realT = "real" stringT :: Bytes stringT = "string" unknownT :: Bytes unknownT = "unknown" data Opt = Opt { _pos :: Properties.T, _name :: Bytes, _typ :: Bytes, _value :: Bytes } newtype T = Options (Map Bytes Opt) {- check -} check_name :: T -> Bytes -> Opt check_name (Options map) name = case Map.lookup name map of Just opt | _typ opt /= unknownT -> opt _ -> error (make_string ("Unknown system option " <> quote name)) check_type :: T -> Bytes -> Bytes -> Opt check_type options name typ = let opt = check_name options name t = _typ opt in if t == typ then opt else error (make_string ("Ill-typed system option " <> quote name <> " : " <> t <> " vs. " <> typ)) {- get typ -} typ :: T -> Bytes -> Bytes typ options name = _typ (check_name options name) {- get value -} get :: Bytes -> (Bytes -> Maybe a) -> T -> Bytes -> a get typ parse options name = let opt = check_type options name typ in case parse (_value opt) of Just x -> x Nothing -> error (make_string ("Malformed value for system option " <> quote name <> " : " <> typ <> " =\n" <> quote (_value opt))) bool :: T -> Bytes -> Bool bool = get boolT Value.parse_bool int :: T -> Bytes -> Int int = get intT Value.parse_int real :: T -> Bytes -> Double real = get realT Value.parse_real seconds :: T -> Bytes -> Time seconds options = Time.seconds . real options string :: T -> Bytes -> Bytes string = get stringT Just {- decode -} instance Decode T where decode :: Decode.T T decode = let decode_entry :: Decode.T (Bytes, Opt) decode_entry body = let (pos, (name, (typ, value))) = Decode.pair Decode.properties (Decode.pair Decode.string (Decode.pair Decode.string Decode.string)) body in (name, Opt { _pos = pos, _name = name, _typ = typ, _value = value }) in Options . Map.fromList . Decode.list decode_entry \ generate_file "Isabelle/Isabelle_System.hs" = \ {- Title: Isabelle/Isabelle_System.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Isabelle system support. See \<^file>\~~/src/Pure/System/isabelle_system.ML\ and \<^file>\~~/src/Pure/System/isabelle_system.scala\ -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Isabelle_System ( bash_process, bash_process0 ) where import Data.Maybe (fromMaybe) import Control.Exception (throw, AsyncException (UserInterrupt)) import Network.Socket (Socket) import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import qualified Isabelle.Byte_Message as Byte_Message import qualified Isabelle.Time as Time import Isabelle.Timing (Timing (..)) import qualified Isabelle.Options as Options import qualified Isabelle.Bash as Bash import qualified Isabelle.Process_Result as Process_Result import qualified Isabelle.XML.Encode as Encode import qualified Isabelle.YXML as YXML import qualified Isabelle.Value as Value import qualified Isabelle.Server as Server import qualified Isabelle.Isabelle_Thread as Isabelle_Thread import Isabelle.Library {- bash_process -} absolute_path :: Bytes -> Bytes -- FIXME dummy absolute_path = id bash_process :: Options.T -> Bash.Params -> IO Process_Result.T bash_process options = bash_process0 address password where address = Options.string options "bash_process_address" password = Options.string options "bash_process_password" bash_process0 :: Bytes -> Bytes -> Bash.Params -> IO Process_Result.T bash_process0 address password params = do Server.connection port password (\socket -> do isabelle_tmp <- getenv "ISABELLE_TMP" Byte_Message.write_message socket (run isabelle_tmp) loop Nothing socket) where port = case Bytes.try_unprefix Server.localhost_prefix address of Just port -> make_string port Nothing -> errorWithoutStackTrace "Bad bash_process server address" script = Bash.get_script params input = Bash.get_input params cwd = Bash.get_cwd params putenv = Bash.get_putenv params redirect = Bash.get_redirect params timeout = Bash.get_timeout params description = Bash.get_description params run :: Bytes -> [Bytes] run isabelle_tmp = [Bash.server_run, script, input, YXML.string_of_body (Encode.option (Encode.string . absolute_path) cwd), YXML.string_of_body (Encode.list (Encode.pair Encode.string Encode.string) (("ISABELLE_TMP", isabelle_tmp) : putenv)), Value.print_bool redirect, Value.print_real (Time.get_seconds timeout), description] kill :: Maybe Bytes -> IO () kill maybe_uuid = do case maybe_uuid of Just uuid -> Server.connection port password (\socket -> Byte_Message.write_message socket [Bash.server_kill, uuid]) Nothing -> return () err = errorWithoutStackTrace "Malformed result from bash_process server" the = fromMaybe err loop :: Maybe Bytes -> Socket -> IO Process_Result.T loop maybe_uuid socket = do result <- Isabelle_Thread.bracket_resource (kill maybe_uuid) (Byte_Message.read_message socket) case result of Just [head, uuid] | head == Bash.server_uuid -> loop (Just uuid) socket Just [head] | head == Bash.server_interrupt -> throw UserInterrupt Just [head, msg] | head == Bash.server_failure -> errorWithoutStackTrace $ make_string msg Just (head : a : b : c : d : lines) | head == Bash.server_result -> let rc = the $ Value.parse_int a elapsed = Time.ms $ the $ Value.parse_int b cpu = Time.ms $ the $ Value.parse_int c timing = Timing elapsed cpu Time.zero n = the $ Value.parse_int d out_lines = take n lines err_lines = drop n lines in return $ Process_Result.make rc out_lines err_lines timing _ -> err \ generate_file "Isabelle/Cache.hs" = \ {- Title: Isabelle/Cache.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Cache for slow computations. -} module Isabelle.Cache ( T, init, apply, prune ) where import Prelude hiding (init) import Data.IORef import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import qualified Data.List as List import Isabelle.Time (Time) import qualified Isabelle.Time as Time data Entry v = Entry {_value :: v, _access :: Time, _timing :: Time} newtype T k v = Cache (IORef (Map k (Entry v))) init :: IO (T k v) init = Cache <$> newIORef Map.empty commit :: Ord k => T k v -> k -> Entry v -> IO v commit (Cache ref) x e = do atomicModifyIORef' ref (\entries -> let entry = case Map.lookup x entries of Just e' | _access e' > _access e -> e' _ -> e in (Map.insert x entry entries, _value entry)) apply :: Ord k => T k v -> k -> IO v -> IO v apply cache@(Cache ref) x body = do start <- Time.now entries <- readIORef ref case Map.lookup x entries of Just entry -> do commit cache x (entry {_access = start}) Nothing -> do y <- body stop <- Time.now commit cache x (Entry y start (stop - start)) prune :: Ord k => T k v -> Int -> Time -> IO () prune (Cache ref) max_size min_timing = do atomicModifyIORef' ref (\entries -> let trim x e = if _timing e < min_timing then Map.delete x else id sort = List.sortBy (\(_, e1) (_, e2) -> compare (_access e2) (_access e1)) entries1 = Map.foldrWithKey trim entries entries entries2 = if Map.size entries1 <= max_size then entries1 else Map.fromList $ List.take max_size $ sort $ Map.toList entries1 in (entries2, ())) \ export_generated_files _ end diff --git a/src/Tools/VSCode/src/vscode_rendering.scala b/src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala +++ b/src/Tools/VSCode/src/vscode_rendering.scala @@ -1,326 +1,316 @@ /* Title: Tools/VSCode/src/vscode_rendering.scala Author: Makarius Isabelle/VSCode-specific implementation of quasi-abstract rendering and markup interpretation. */ package isabelle.vscode import isabelle._ import java.io.{File => JFile} import scala.annotation.tailrec object VSCode_Rendering { /* decorations */ private def color_decorations( prefix: String, types: Set[Rendering.Color.Value], colors: List[Text.Info[Rendering.Color.Value]] ): List[VSCode_Model.Decoration] = { val color_ranges = colors.foldLeft(Map.empty[Rendering.Color.Value, List[Text.Range]]) { case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil))) } types.toList.map(c => VSCode_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse)) } private val background_colors = Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result - Rendering.Color.entity private val dotted_colors = Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning) /* diagnostic messages */ private val message_severity = Map( Markup.LEGACY -> LSP.DiagnosticSeverity.Warning, Markup.ERROR -> LSP.DiagnosticSeverity.Error) /* markup elements */ private val diagnostics_elements = Markup.Elements(Markup.LEGACY, Markup.ERROR) private val background_elements = Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements private val dotted_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING) val tooltip_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.BAD) ++ Rendering.tooltip_elements private val hyperlink_elements = - Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION) + Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION) } class VSCode_Rendering(snapshot: Document.Snapshot, val model: VSCode_Model) extends Rendering(snapshot, model.resources.options, model.session) { rendering => def resources: VSCode_Resources = model.resources override def get_text(range: Text.Range): Option[String] = model.get_text(range) /* completion */ def completion(node_pos: Line.Node_Position, caret: Text.Offset): List[LSP.CompletionItem] = { val doc = model.content.doc val line = node_pos.pos.line val unicode = File.is_thy(node_pos.name) doc.offset(Line.Position(line)) match { case None => Nil case Some(line_start) => val history = Completion.History.empty val caret_range = before_caret_range(caret) val syntax = model.syntax() val syntax_completion = syntax.complete(history, unicode, explicit = false, line_start, doc.lines(line).text, caret - line_start, language_context(caret_range) getOrElse syntax.language_context) val (no_completion, semantic_completion) = rendering.semantic_completion_result( history, unicode, syntax_completion.map(_.range), caret_range) if (no_completion) Nil else { val results = Completion.Result.merge(history, semantic_completion, syntax_completion, VSCode_Spell_Checker.completion(rendering, caret), - path_completion(caret), - model.editor.bibtex_completion(history, rendering, caret)) + path_completion(caret)) val items = results match { case None => Nil case Some(result) => result.items.map(item => LSP.CompletionItem( label = item.description.mkString(" "), text = Some(item.replacement), range = Some(doc.range(item.range)))) } items ::: VSCode_Spell_Checker.menu_items(rendering, caret) } } } /* diagnostics */ def diagnostics: List[Text.Info[Command.Results]] = snapshot.cumulate[Command.Results]( model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, command_states => { case (res, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body))) if body.nonEmpty => Some(res + (i -> msg)) case (res, Text.Info(_, msg)) => Command.State.get_result_proper(command_states, msg.markup.properties).map(res + _) }).filterNot(info => info.info.is_empty) def diagnostics_output(results: List[Text.Info[Command.Results]]): List[LSP.Diagnostic] = { (for { Text.Info(text_range, res) <- results.iterator range = model.content.doc.range(text_range) (_, XML.Elem(Markup(name, _), body)) <- res.iterator } yield { val message = resources.output_pretty_message(body) val severity = VSCode_Rendering.message_severity.get(name) LSP.Diagnostic(range, message, severity = severity) }).toList } /* text color */ def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = { snapshot.select(range, Rendering.text_color_elements, _ => { case Text.Info(_, XML.Elem(Markup(name, props), _)) => if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None else Rendering.text_color.get(name) }) } /* text overview color */ private sealed case class Color_Info( color: Rendering.Color.Value, offset: Text.Offset, end_offset: Text.Offset, end_line: Int) def text_overview_color: List[Text.Info[Rendering.Color.Value]] = { @tailrec def loop( offset: Text.Offset, line: Int, lines: List[Line], colors: List[Color_Info] ): List[Text.Info[Rendering.Color.Value]] = { if (lines.nonEmpty) { val end_offset = offset + lines.head.text.length val colors1 = (overview_color(Text.Range(offset, end_offset)), colors) match { case (Some(color), old :: rest) if color == old.color && line == old.end_line => old.copy(end_offset = end_offset, end_line = line + 1) :: rest case (Some(color), _) => Color_Info(color, offset, end_offset, line + 1) :: colors case (None, _) => colors } loop(end_offset + 1, line + 1, lines.tail, colors1) } else { colors.reverse.map(info => Text.Info(Text.Range(info.offset, info.end_offset), info.color)) } } loop(0, 0, model.content.doc.lines, Nil) } /* dotted underline */ def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = message_underline_color(VSCode_Rendering.dotted_elements, range) /* decorations */ def decorations: List[VSCode_Model.Decoration] = // list of canonical length and order Par_List.map((f: () => List[VSCode_Model.Decoration]) => f(), List( () => VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors, background(VSCode_Rendering.background_elements, model.content.text_range, Rendering.Focus.empty)), () => VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors, foreground(model.content.text_range)), () => VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors, text_color(model.content.text_range)), () => VSCode_Rendering.color_decorations("text_overview_", Rendering.Color.text_overview_colors, text_overview_color), () => VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors, dotted(model.content.text_range)))).flatten ::: List(VSCode_Spell_Checker.decoration(rendering)) def decoration_output(decoration: List[VSCode_Model.Decoration]): LSP.Decoration = { val entries = for (deco <- decoration) yield { val decopts = for(Text.Info(text_range, msgs) <- deco.content) yield { val range = model.content.doc.range(text_range) LSP.Decoration_Options(range, msgs.map(msg => LSP.MarkedString(resources.output_pretty_tooltip(msg)))) } (deco.typ, decopts) } LSP.Decoration(entries) } /* tooltips */ override def timing_threshold: Double = options.real("vscode_timing_threshold") /* hyperlinks */ def hyperlink_source_file( source_name: String, line1: Int, range: Symbol.Range ): Option[Line.Node_Range] = { for { platform_path <- resources.source_file(source_name) file <- (try { Some(File.absolute(new JFile(platform_path))) } catch { case ERROR(_) => None }) } yield { Line.Node_Range(file.getPath, if (range.start > 0) { resources.get_file_content(resources.node_name(file)) match { case Some(text) => val chunk = Symbol.Text_Chunk(text) val doc = Line.Document(text) doc.range(chunk.decode(range)) case _ => Line.Range(Line.Position((line1 - 1) max 0)) } } else Line.Range(Line.Position((line1 - 1) max 0))) } } def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] = { if (snapshot.is_outdated) None else for { start <- snapshot.find_command_position(id, range.start) stop <- snapshot.find_command_position(id, range.stop) } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos)) } def hyperlink_position(pos: Position.T): Option[Line.Node_Range] = pos match { case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range) case Position.Item_Id(id, range) => hyperlink_command(id, range) case _ => None } def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] = pos match { case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range) case Position.Item_Def_Id(id, range) => hyperlink_command(id, range) case _ => None } def hyperlinks(range: Text.Range): List[Line.Node_Range] = { snapshot.cumulate[List[Line.Node_Range]]( range, Nil, VSCode_Rendering.hyperlink_elements, _ => { case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => val file = perhaps_append_file(snapshot.node_name, name) Some(Line.Node_Range(file) :: links) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => hyperlink_def_position(props).map(_ :: links) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => hyperlink_position(props).map(_ :: links) - case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => - val iterator = - for { - Text.Info(entry_range, (entry, model: VSCode_Model)) <- - model.editor.bibtex_entries_iterator() - if entry == name - } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range)) - if (iterator.isEmpty) None else Some(iterator.foldLeft(links)(_ :+ _)) - case _ => None }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } } } diff --git a/src/Tools/jEdit/src/completion_popup.scala b/src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala +++ b/src/Tools/jEdit/src/completion_popup.scala @@ -1,678 +1,676 @@ /* Title: Tools/jEdit/src/completion_popup.scala Author: Makarius Completion popup. */ package isabelle.jedit import isabelle._ import java.awt.{Color, Font, Point, BorderLayout, Dimension} import java.awt.event.{KeyEvent, KeyListener, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} import java.io.{File => JFile} import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities} import javax.swing.border.LineBorder import javax.swing.text.DefaultCaret import scala.swing.{ListView, ScrollPane} import scala.swing.event.MouseClicked import org.gjt.sp.jedit.View import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection} import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround} import org.gjt.sp.util.StandardUtilities object Completion_Popup { /** items with HTML rendering **/ private class Item(val item: Completion.Item) { private val html = item.description match { case a :: bs => "" + HTML.output(Symbol.print_newlines(a)) + "" + HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "" case Nil => "" } override def toString: String = html } /** jEdit text area **/ object Text_Area { private val key = new Object def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] = { GUI_Thread.require {} text_area.getClientProperty(key) match { case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion) case _ => None } } def active_range(text_area: TextArea): Option[Text.Range] = apply(text_area) match { case Some(text_area_completion) => text_area_completion.active_range case None => None } def action(text_area: TextArea, word_only: Boolean): Boolean = apply(text_area) match { case Some(text_area_completion) => if (text_area_completion.active_range.isDefined) text_area_completion.action(word_only = word_only) else text_area_completion.action(immediate = true, explicit = true, word_only = word_only) true case None => false } def exit(text_area: JEditTextArea): Unit = { GUI_Thread.require {} apply(text_area) match { case None => case Some(text_area_completion) => text_area_completion.deactivate() text_area.putClientProperty(key, null) } } def init(text_area: JEditTextArea): Completion_Popup.Text_Area = { exit(text_area) val text_area_completion = new Text_Area(text_area) text_area.putClientProperty(key, text_area_completion) text_area_completion.activate() text_area_completion } def dismissed(text_area: TextArea): Boolean = { GUI_Thread.require {} apply(text_area) match { case Some(text_area_completion) => text_area_completion.dismissed() case None => false } } } class Text_Area private(text_area: JEditTextArea) { // owned by GUI thread private var completion_popup: Option[Completion_Popup] = None def active_range: Option[Text.Range] = completion_popup match { case Some(completion) => completion.active_range case None => None } /* rendering */ def rendering(rendering: JEdit_Rendering, line_range: Text.Range): Option[Text.Info[Color]] = { active_range match { case Some(range) => range.try_restrict(line_range) case None => val caret = text_area.getCaretPosition if (line_range.contains(caret)) { rendering.before_caret_range(caret).try_restrict(line_range) match { case Some(range) if !range.is_singularity => val range0 = Completion.Result.merge(Completion.History.empty, syntax_completion(Completion.History.empty, true, Some(rendering)), - rendering.path_completion(caret), - PIDE.editor.bibtex_completion(Completion.History.empty, rendering, caret)) + rendering.path_completion(caret)) .map(_.range) rendering.semantic_completion(range0, range) match { case None => range0 case Some(Text.Info(_, Completion.No_Completion)) => None case Some(Text.Info(range1, _: Completion.Names)) => Some(range1) } case _ => None } } else None } }.map(range => Text.Info(range, rendering.completion_color)) /* syntax completion */ def syntax_completion( history: Completion.History, explicit: Boolean, opt_rendering: Option[JEdit_Rendering] ): Option[Completion.Result] = { val buffer = text_area.getBuffer val unicode = Isabelle_Encoding.is_active(buffer) Isabelle.buffer_syntax(buffer) match { case Some(syntax) => val context = (for { rendering <- opt_rendering if PIDE.options.bool("jedit_completion_context") caret_range = rendering.before_caret_range(text_area.getCaretPosition) context <- rendering.language_context(caret_range) } yield context) getOrElse syntax.language_context val caret = text_area.getCaretPosition val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine) val line_start = line_range.start for { line_text <- JEdit_Lib.get_text(buffer, line_range) result <- syntax.complete( history, unicode, explicit, line_start, line_text, caret - line_start, context) } yield result case None => None } } /* completion action: text area */ private def insert(item: Completion.Item): Unit = { GUI_Thread.require {} val buffer = text_area.getBuffer val range = item.range if (buffer.isEditable) { JEdit_Lib.buffer_edit(buffer) { JEdit_Lib.get_text(buffer, range) match { case Some(text) if text == item.original => text_area.getSelectionAtOffset(text_area.getCaretPosition) match { /*rectangular selection as "tall caret"*/ case selection : Selection.Rect if selection.getStart(buffer, text_area.getCaretLine) == range.stop => text_area.moveCaretPosition(range.stop) (0 until Character.codePointCount(item.original, 0, item.original.length)) .foreach(_ => text_area.backspace()) text_area.setSelectedText(selection, item.replacement) text_area.moveCaretPosition(text_area.getCaretPosition + item.move) /*other selections: rectangular, multiple range, ...*/ case selection if selection != null && selection.getStart(buffer, text_area.getCaretLine) == range.start && selection.getEnd(buffer, text_area.getCaretLine) == range.stop => text_area.moveCaretPosition(range.stop + item.move) text_area.getSelection.foreach(text_area.setSelectedText(_, item.replacement)) /*no selection*/ case _ => buffer.remove(range.start, range.length) buffer.insert(range.start, item.replacement) text_area.moveCaretPosition(range.start + item.replacement.length + item.move) Isabelle.indent_input(text_area) } case _ => } } } } def action( immediate: Boolean = false, explicit: Boolean = false, delayed: Boolean = false, word_only: Boolean = false ): Boolean = { val view = text_area.getView val layered = view.getLayeredPane val buffer = text_area.getBuffer val painter = text_area.getPainter val history = PIDE.plugin.completion_history.value val unicode = Isabelle_Encoding.is_active(buffer) def open_popup(result: Completion.Result): Unit = { val font = painter.getFont.deriveFont( Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale"))) val range = result.range val loc1 = text_area.offsetToXY(range.start) if (loc1 != null) { val loc2 = SwingUtilities.convertPoint(painter, loc1.x, loc1.y + painter.getLineHeight, layered) val items = result.items.map(new Item(_)) val completion = new Completion_Popup(Some(range), layered, loc2, font, items) { override def complete(item: Completion.Item): Unit = { PIDE.plugin.completion_history.update(item) insert(item) } override def propagate(evt: KeyEvent): Unit = { if (view.getKeyEventInterceptor == null) JEdit_Lib.propagate_key(view, evt) else if (view.getKeyEventInterceptor == inner_key_listener) { try { view.setKeyEventInterceptor(null) JEdit_Lib.propagate_key(view, evt) } finally { if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener) } } if (evt.getID == KeyEvent.KEY_TYPED) input(evt) } override def shutdown(focus: Boolean): Unit = { if (view.getKeyEventInterceptor == inner_key_listener) view.setKeyEventInterceptor(null) if (focus) text_area.requestFocus() JEdit_Lib.invalidate_range(text_area, range) } } dismissed() completion_popup = Some(completion) view.setKeyEventInterceptor(completion.inner_key_listener) JEdit_Lib.invalidate_range(text_area, range) Pretty_Tooltip.dismissed_all() completion.show_popup(false) } } if (buffer.isEditable) { val caret = text_area.getCaretPosition val opt_rendering = Document_View.get_rendering(text_area) val result0 = syntax_completion(history, explicit, opt_rendering) val (no_completion, semantic_completion) = { opt_rendering match { case Some(rendering) => rendering.semantic_completion_result(history, unicode, result0.map(_.range), rendering.before_caret_range(caret)) case None => (false, None) } } if (no_completion) false else { val result = { val result1 = if (word_only) None else Completion.Result.merge(history, semantic_completion, result0) opt_rendering match { case None => result1 case Some(rendering) => Completion.Result.merge(history, result1, JEdit_Spell_Checker.completion(rendering, explicit, caret), - rendering.path_completion(caret), - PIDE.editor.bibtex_completion(history, rendering, caret)) + rendering.path_completion(caret)) } } result match { case Some(result) => result.items match { case List(item) if result.unique && item.immediate && immediate => insert(item) true case _ :: _ if !delayed => open_popup(result) false case _ => false } case None => false } } } else false } /* input key events */ def input(evt: KeyEvent): Unit = { GUI_Thread.require {} if (!evt.isConsumed) { val special = JEdit_Lib.special_key(evt) if (PIDE.options.bool("jedit_completion")) { dismissed() if (evt.getKeyChar != '\b') { val immediate = PIDE.options.bool("jedit_completion_immediate") if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { input_delay.revoke() action(immediate = immediate) } else { if (!special && action(immediate = immediate, delayed = true)) input_delay.revoke() else input_delay.invoke() } } } val selection = text_area.getSelection() if (!special && (selection == null || selection.isEmpty)) Isabelle.indent_input(text_area) } } private val input_delay = Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) { action() } /* dismiss popup */ def dismissed(): Boolean = { GUI_Thread.require {} completion_popup match { case Some(completion) => completion.hide_popup() completion_popup = None true case None => false } } /* activation */ private val outer_key_listener = JEdit_Lib.key_listener(key_typed = input) private def activate(): Unit = text_area.addKeyListener(outer_key_listener) private def deactivate(): Unit = { dismissed() text_area.removeKeyListener(outer_key_listener) } } /** history text field **/ class History_Text_Field( name: String = null, instant_popups: Boolean = false, enter_adds_to_history: Boolean = true, syntax: Outer_Syntax = Outer_Syntax.empty) extends HistoryTextField(name, instant_popups, enter_adds_to_history ) { text_field => // see https://forums.oracle.com/thread/1361677 if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret) // owned by GUI thread private var completion_popup: Option[Completion_Popup] = None /* dismiss */ private def dismissed(): Boolean = { completion_popup match { case Some(completion) => completion.hide_popup() completion_popup = None true case None => false } } /* insert */ private def insert(item: Completion.Item): Unit = { GUI_Thread.require {} val range = item.range if (text_field.isEditable) { val content = text_field.getText range.try_substring(content) match { case Some(text) if text == item.original => text_field.setText( content.substring(0, range.start) + item.replacement + content.substring(range.stop)) text_field.getCaret.setDot(range.start + item.replacement.length + item.move) case _ => } } } /* completion action: text field */ def action(): Unit = { GUI.layered_pane(text_field) match { case Some(layered) if text_field.isEditable => val history = PIDE.plugin.completion_history.value val caret = text_field.getCaret.getDot val text = text_field.getText val context = syntax.language_context syntax.complete(history, true, false, 0, text, caret, context) match { case Some(result) => val fm = text_field.getFontMetrics(text_field.getFont) val loc = SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered) val items = result.items.map(new Item(_)) val completion = new Completion_Popup(None, layered, loc, text_field.getFont, items) { override def complete(item: Completion.Item): Unit = { PIDE.plugin.completion_history.update(item) insert(item) } override def propagate(evt: KeyEvent): Unit = if (!evt.isConsumed) text_field.processKeyEvent(evt) override def shutdown(focus: Boolean): Unit = if (focus) text_field.requestFocus() } dismissed() completion_popup = Some(completion) completion.show_popup(true) case None => } case _ => } } /* process key event */ private def process(evt: KeyEvent): Unit = { if (PIDE.options.bool("jedit_completion")) { dismissed() if (evt.getKeyChar != '\b') { val special = JEdit_Lib.special_key(evt) if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { process_delay.revoke() action() } else process_delay.invoke() } } } private val process_delay = Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) { action() } override def processKeyEvent(evt0: KeyEvent): Unit = { val evt = KeyEventWorkaround.processKeyEvent(evt0) if (evt != null) { evt.getID match { case KeyEvent.KEY_PRESSED => val key_code = evt.getKeyCode if (key_code == KeyEvent.VK_ESCAPE) { if (dismissed()) evt.consume() } case KeyEvent.KEY_TYPED => super.processKeyEvent(evt) process(evt) evt.consume() case _ => } if (!evt.isConsumed) super.processKeyEvent(evt) } } } } class Completion_Popup private( opt_range: Option[Text.Range], layered: JLayeredPane, location: Point, font: Font, items: List[Completion_Popup.Item] ) extends JPanel(new BorderLayout) { completion => GUI_Thread.require {} require(items.nonEmpty, "no completion items") val multi: Boolean = items.length > 1 /* actions */ def complete(item: Completion.Item): Unit = {} def propagate(evt: KeyEvent): Unit = {} def shutdown(focus: Boolean): Unit = {} /* list view */ private val list_view = new ListView(items) list_view.font = font list_view.selection.intervalMode = ListView.IntervalMode.Single list_view.peer.setFocusTraversalKeysEnabled(false) list_view.peer.setVisibleRowCount(items.length min 8) list_view.peer.setSelectedIndex(0) for (cond <- List(JComponent.WHEN_FOCUSED, JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, JComponent.WHEN_IN_FOCUSED_WINDOW)) list_view.peer.setInputMap(cond, null) private def complete_selected(): Boolean = { list_view.selection.items.toList match { case item :: _ => complete(item.item); true case _ => false } } private def move_items(n: Int): Unit = { val i = list_view.peer.getSelectedIndex val j = ((i + n) min (items.length - 1)) max 0 if (i != j) { list_view.peer.setSelectedIndex(j) list_view.peer.ensureIndexIsVisible(j) } } private def move_pages(n: Int): Unit = { val page_size = list_view.peer.getVisibleRowCount - 1 move_items(page_size * n) } /* event handling */ val inner_key_listener: KeyListener = JEdit_Lib.key_listener( key_pressed = { (e: KeyEvent) => if (!e.isConsumed) { e.getKeyCode match { case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") => if (complete_selected()) e.consume() hide_popup() case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") => if (complete_selected()) e.consume() hide_popup() case KeyEvent.VK_ESCAPE => hide_popup() e.consume() case KeyEvent.VK_UP | KeyEvent.VK_KP_UP if multi => move_items(-1) e.consume() case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN if multi => move_items(1) e.consume() case KeyEvent.VK_PAGE_UP if multi => move_pages(-1) e.consume() case KeyEvent.VK_PAGE_DOWN if multi => move_pages(1) e.consume() case _ => if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) hide_popup() } } propagate(e) }, key_typed = propagate ) list_view.peer.addKeyListener(inner_key_listener) list_view.peer.addMouseListener(new MouseAdapter { override def mouseClicked(e: MouseEvent): Unit = { if (complete_selected()) e.consume() hide_popup() } }) list_view.peer.addFocusListener(new FocusAdapter { override def focusLost(e: FocusEvent): Unit = hide_popup() }) /* main content */ override def getFocusTraversalKeysEnabled = false completion.setBorder(new LineBorder(Color.BLACK)) completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent]) /* popup */ def active_range: Option[Text.Range] = if (isDisplayable) opt_range else None private val popup = { val screen = GUI.screen_location(layered, location) val size = { val geometry = JEdit_Lib.window_geometry(completion, completion) val bounds = JEdit_Rendering.popup_bounds val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight new Dimension(w, h) } new Popup(layered, completion, screen.relative(layered, size), size) } private def show_popup(focus: Boolean): Unit = { popup.show if (focus) list_view.requestFocus() } private def hide_popup(): Unit = { shutdown(list_view.peer.isFocusOwner) popup.hide } } diff --git a/src/Tools/jEdit/src/jedit_rendering.scala b/src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala +++ b/src/Tools/jEdit/src/jedit_rendering.scala @@ -1,417 +1,410 @@ /* Title: Tools/jEdit/src/jedit_rendering.scala Author: Makarius Isabelle/jEdit-specific implementation of quasi-abstract rendering and markup interpretation. */ package isabelle.jedit import isabelle._ import java.awt.Color import javax.swing.Icon import org.gjt.sp.jedit.syntax.{Token => JEditToken} import org.gjt.sp.jedit.jEdit import scala.collection.immutable.SortedMap object JEdit_Rendering { /* make rendering */ def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering = new JEdit_Rendering(snapshot, model, options) def text( snapshot: Document.Snapshot, formatted_body: XML.Body, results: Command.Results = Command.Results.empty ): (String, JEdit_Rendering) = { val command = Command.rich_text(Document_ID.make(), results, formatted_body) val snippet = snapshot.snippet(command, Document.Blobs.empty) val model = File_Model.init(PIDE.session) val rendering = apply(snippet, model, PIDE.options.value) (command.source, rendering) } /* popup window bounds */ def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8 /* Isabelle/Isar token markup */ private val command_style: Map[String, Byte] = { import JEditToken._ Map[String, Byte]( Keyword.THY_END -> KEYWORD2, Keyword.PRF_ASM -> KEYWORD3, Keyword.PRF_ASM_GOAL -> KEYWORD3 ).withDefaultValue(KEYWORD1) } private val token_style: Map[Token.Kind.Value, Byte] = { import JEditToken._ Map[Token.Kind.Value, Byte]( Token.Kind.KEYWORD -> KEYWORD2, Token.Kind.IDENT -> NULL, Token.Kind.LONG_IDENT -> NULL, Token.Kind.SYM_IDENT -> NULL, Token.Kind.VAR -> NULL, Token.Kind.TYPE_IDENT -> NULL, Token.Kind.TYPE_VAR -> NULL, Token.Kind.NAT -> NULL, Token.Kind.FLOAT -> NULL, Token.Kind.SPACE -> NULL, Token.Kind.STRING -> LITERAL1, Token.Kind.ALT_STRING -> LITERAL2, Token.Kind.CARTOUCHE -> COMMENT3, Token.Kind.CONTROL -> COMMENT3, Token.Kind.INFORMAL_COMMENT -> COMMENT1, Token.Kind.FORMAL_COMMENT -> COMMENT1, Token.Kind.ERROR -> INVALID ).withDefaultValue(NULL) } def token_markup(syntax: Outer_Syntax, token: Token): Byte = if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, "")) else if (token.is_delimiter) JEditToken.OPERATOR else token_style(token.kind) /* Isabelle/ML token markup */ private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] = { import JEditToken._ Map[ML_Lex.Kind.Value, Byte]( ML_Lex.Kind.KEYWORD -> NULL, ML_Lex.Kind.IDENT -> NULL, ML_Lex.Kind.LONG_IDENT -> NULL, ML_Lex.Kind.TYPE_VAR -> NULL, ML_Lex.Kind.WORD -> DIGIT, ML_Lex.Kind.INT -> DIGIT, ML_Lex.Kind.REAL -> DIGIT, ML_Lex.Kind.CHAR -> LITERAL2, ML_Lex.Kind.STRING -> LITERAL1, ML_Lex.Kind.SPACE -> NULL, ML_Lex.Kind.INFORMAL_COMMENT -> COMMENT1, ML_Lex.Kind.FORMAL_COMMENT -> COMMENT1, ML_Lex.Kind.ANTIQ -> NULL, ML_Lex.Kind.ANTIQ_START -> LITERAL4, ML_Lex.Kind.ANTIQ_STOP -> LITERAL4, ML_Lex.Kind.ANTIQ_OTHER -> NULL, ML_Lex.Kind.ANTIQ_STRING -> NULL, ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL, ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL, ML_Lex.Kind.ERROR -> INVALID ).withDefaultValue(NULL) } def ml_token_markup(token: ML_Lex.Token): Byte = if (!token.is_keyword) ml_token_style(token.kind) else if (token.is_delimiter) JEditToken.OPERATOR else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2 else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3 else JEditToken.KEYWORD1 /* markup elements */ private val indentation_elements = Markup.Elements(Markup.Command_Indent.name) private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT) private val highlight_elements = - Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, + Markup.Elements(Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT, Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) private val hyperlink_elements = Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.EXPORT_PATH, Markup.DOC, Markup.URL, - Markup.POSITION, Markup.CITATION) + Markup.POSITION) private val gutter_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) private val squiggly_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) private val line_background_elements = Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE, Markup.ERROR_MESSAGE) private val separator_elements = Markup.Elements(Markup.SEPARATOR) private val bullet_elements = Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT) private val fold_depth_elements = Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL) } class JEdit_Rendering(snapshot: Document.Snapshot, model: Document_Model, options: Options) extends Rendering(snapshot, options, PIDE.session) { override def get_text(range: Text.Range): Option[String] = model.get_text(range) /* colors */ def color(s: String): Color = if (s == "main_color") main_color else Color_Value(options.string(s)) def color(c: Rendering.Color.Value): Color = _rendering_colors(c) lazy val _rendering_colors: Map[Rendering.Color.Value, Color] = Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap val main_color = jEdit.getColorProperty("view.fgColor") val outdated_color = color("outdated_color") val bullet_color = color("bullet_color") val tooltip_color = color("tooltip_color") val spell_checker_color = color("spell_checker_color") val entity_ref_color = color("entity_ref_color") val breakpoint_disabled_color = color("breakpoint_disabled_color") val breakpoint_enabled_color = color("breakpoint_enabled_color") val caret_debugger_color = color("caret_debugger_color") val highlight_color = color("highlight_color") val hyperlink_color = color("hyperlink_color") val active_hover_color = color("active_hover_color") val caret_invisible_color = color("caret_invisible_color") val completion_color = color("completion_color") val search_color = color("search_color") /* indentation */ def indentation(range: Text.Range): Int = snapshot.select(range, JEdit_Rendering.indentation_elements, _ => { case Text.Info(_, XML.Elem(Markup.Command_Indent(i), _)) => Some(i) case _ => None }).headOption.map(_.info).getOrElse(0) /* breakpoints */ def breakpoint(range: Text.Range): Option[(Command, Long)] = if (snapshot.is_outdated) None else snapshot.select(range, JEdit_Rendering.breakpoint_elements, command_states => { case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) => command_states match { case st :: _ => Some((st.command, breakpoint)) case _ => None } case _ => None }).headOption.map(_.info) /* caret focus */ def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] = snapshot.select(range, Rendering.entity_elements, _ => { case Text.Info(_, XML.Elem(Markup.Entity.Ref(i), _)) if focus(i) => Some(entity_ref_color) case _ => None }) /* highlighted area */ def highlight(range: Text.Range): Option[Text.Info[Color]] = snapshot.select(range, JEdit_Rendering.highlight_elements, _ => { case info => Some(Text.Info(snapshot.convert(info.range), highlight_color)) }).headOption.map(_.info) /* hyperlinks */ def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = { snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]]( range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ => { case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) => val file = perhaps_append_file(snapshot.node_name, name) val link = PIDE.editor.hyperlink_file(true, file) Some(links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup.Export_Path(name), _))) => val link = PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name) Some(links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) => PIDE.editor.hyperlink_doc(name).map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) => val link = PIDE.editor.hyperlink_url(name) Some(links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props) opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) - case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => - val opt_link = - PIDE.editor.bibtex_entries_iterator().collectFirst( - { case Text.Info(entry_range, (entry, model: Document_Model)) if entry == name => - PIDE.editor.hyperlink_model(true, model, entry_range.start) }) - opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) - case _ => None }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } } def hyperlink_entity(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = { snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]]( range, Vector.empty, Rendering.entity_elements, _ => { case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) case _ => None }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } } /* active elements */ def active(range: Text.Range): Option[Text.Info[XML.Elem]] = snapshot.select(range, Rendering.active_elements, command_states => { case Text.Info(info_range, elem) => if (elem.name == Markup.DIALOG) { elem match { case Protocol.Dialog(_, serial, _) if !command_states.exists(st => st.results.defined(serial)) => Some(Text.Info(snapshot.convert(info_range), elem)) case _ => None } } else Some(Text.Info(snapshot.convert(info_range), elem)) }).headOption.map(_.info) /* tooltips */ def tooltip_margin: Int = options.int("jedit_tooltip_margin") override def timing_threshold: Double = options.real("jedit_timing_threshold") def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[XML.Body]] = { val elements = if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements tooltips(elements, range).map(info => info.map(Pretty.fbreaks)) } lazy val tooltip_close_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon")) lazy val tooltip_detach_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon")) /* gutter */ private def gutter_message_pri(msg: XML.Tree): Int = if (Protocol.is_error(msg)) Rendering.error_pri else if (Protocol.is_legacy(msg)) Rendering.legacy_pri else if (Protocol.is_warning(msg)) Rendering.warning_pri else if (Protocol.is_information(msg)) Rendering.information_pri else 0 private lazy val gutter_message_content = Map( Rendering.information_pri -> (JEdit_Lib.load_icon(options.string("gutter_information_icon")), color(Rendering.Color.information_message)), Rendering.warning_pri -> (JEdit_Lib.load_icon(options.string("gutter_warning_icon")), color(Rendering.Color.warning_message)), Rendering.legacy_pri -> (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), color(Rendering.Color.legacy_message)), Rendering.error_pri -> (JEdit_Lib.load_icon(options.string("gutter_error_icon")), color(Rendering.Color.error_message))) def gutter_content(range: Text.Range): Option[(Icon, Color)] = { val pris = snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ => { case (pri, Text.Info(_, elem)) => Some(pri max gutter_message_pri(elem)) }).map(_.info) gutter_message_content.get(pris.foldLeft(0)(_ max _)) } /* message output */ def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = message_underline_color(JEdit_Rendering.squiggly_elements, range) def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] = { val results = snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ => { case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) }) val pri = results.foldLeft(0) { case (p1, Text.Info(_, p2)) => p1 max p2 } Rendering.message_background_color.get(pri).map(message_color => { val is_separator = snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ => { case _ => Some(true) }).exists(_.info) (message_color, is_separator) }) } /* text color */ def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] = { if (current_color == Syntax_Style.hidden_color) List(Text.Info(range, current_color)) else snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ => { case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color) }) } /* virtual bullets */ def bullet(range: Text.Range): List[Text.Info[Color]] = snapshot.select(range, JEdit_Rendering.bullet_elements, _ => { case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) => PIDE.session.debugger.active_breakpoint_state(breakpoint).map(b => if (b) breakpoint_enabled_color else breakpoint_disabled_color) case _ => Some(bullet_color) }) /* text folds */ def fold_depth(range: Text.Range): List[Text.Info[Int]] = snapshot.cumulate[Int](range, 0, JEdit_Rendering.fold_depth_elements, _ => { case (depth, _) => Some(depth + 1) }) }