# HG changeset patch # User wenzelm # Date 1497001142 -7200 # Node ID f8c4442bb3a95429f6563f2bf1ec18a3f92e6235 # Parent de6cd60b12262be9b05e628eaa05989ad79e5227# Parent bd75167090514adbcc3e0d5488541b4637423f12 merged diff -r de6cd60b1226 -r f8c4442bb3a9 etc/isabelle.css --- a/etc/isabelle.css Thu Jun 08 23:37:01 2017 +0200 +++ b/etc/isabelle.css Fri Jun 09 11:39:02 2017 +0200 @@ -7,7 +7,10 @@ font-weight: bold; } -body { background-color: #FFFFFF; } +body { + color: #000000; + background-color: #FFFFFF; +} .head { background-color: #FFFFFF; } .source { @@ -32,23 +35,30 @@ .binding { color: #336655; } .tfree { color: #A020F0; } .tvar { color: #A020F0; } -.free { color: blue; } +.free { color: #0000FF; } .skolem { color: #D2691E; } -.bound { color: green; } +.bound { color: #008000; } .var { color: #00009B; } .numeral { } .literal { font-weight: bold; } .delimiter { } -.inner_string { color: #FF00CC; } +.inner_numeral { color: #FF0000; } +.inner_quoted { color: #FF00CC; } .inner_cartouche { color: #CC6600; } .inner_comment { color: #CC0000; } +.dynamic { color: #7BA428; } +.class_parameter_color { color: #D2691E; } .bold { font-weight: bold; } -.keyword1 { color: #006699; font-weight: bold; } -.keyword2 { color: #009966; font-weight: bold; } -.keyword3 { color: #0099FF; font-weight: bold; } -.operator { } +.main { color: #000000; } +.command { font-weight: bold; } +.keyword { font-weight: bold; } +.keyword1 { color: #006699; } +.keyword2 { color: #009966; } +.keyword3 { color: #0099FF; } +.quasi_keyword { color: #9966FF; } +.operator { color: #323232; } .string { color: #FF00CC; } .alt_string { color: #CC00CC; } .verbatim { color: #6600CC; } diff -r de6cd60b1226 -r f8c4442bb3a9 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Pure/Isar/token.ML Fri Jun 09 11:39:02 2017 +0200 @@ -293,6 +293,8 @@ fun keyword_markup (important, keyword) x = if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter; +val keyword_properties = Markup.properties [(Markup.kindN, Markup.keywordN)]; + fun completion_report tok = if is_kind Keyword tok then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok)) @@ -302,7 +304,8 @@ if is_command tok then keyword_reports tok (command_markups keywords (content_of tok)) else if is_kind Keyword tok then - keyword_reports tok [keyword_markup (false, Markup.keyword2) (content_of tok)] + keyword_reports tok + [keyword_markup (false, keyword_properties Markup.keyword2) (content_of tok)] else let val (m, text) = token_kind_markup (kind_of tok) in [((pos_of tok, m), text)] end; diff -r de6cd60b1226 -r f8c4442bb3a9 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Pure/PIDE/document.scala Fri Jun 09 11:39:02 2017 +0200 @@ -452,10 +452,13 @@ def node_name: Node.Name def node: Node + def commands_loading: List[Command] def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] + def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body + def find_command(id: Document_ID.Generic): Option[(Node, Command)] def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset) : Option[Line.Node_Position] @@ -769,13 +772,20 @@ range: Text.Range, elements: Markup.Elements): Markup_Tree = Command.State.merge_markup(command_states(version, command), index, range, elements) - def markup_to_XML(version: Version, node: Node, elements: Markup.Elements): XML.Body = + def markup_to_XML( + version: Version, + node: Node, + range: Text.Range, + elements: Markup.Elements): XML.Body = + { (for { command <- node.commands.iterator + command_range <- command.range.try_restrict(range).iterator markup = - command_markup(version, command, Command.Markup_Index.markup, command.range, elements) - tree <- markup.to_XML(command.range, command.source, elements) + command_markup(version, command, Command.Markup_Index.markup, command_range, elements) + tree <- markup.to_XML(command_range, command.source, elements).iterator } yield tree).toList + } // persistent user-view def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil) @@ -845,6 +855,9 @@ } else version.nodes.commands_loading(other_node_name).headOption + def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body = + state.markup_to_XML(version, node, range, elements) + /* find command */ diff -r de6cd60b1226 -r f8c4442bb3a9 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Pure/PIDE/markup.ML Fri Jun 09 11:39:02 2017 +0200 @@ -125,7 +125,8 @@ val markdown_itemN: string val markdown_item: int -> T val inputN: string val input: bool -> Properties.T -> T val command_keywordN: string val command_keyword: T - val commandN: string val command: T + val commandN: string + val keywordN: string val stringN: string val string: T val alt_stringN: string val alt_string: T val verbatimN: string val verbatim: T @@ -304,7 +305,7 @@ (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)])); fun get_entity_kind (name, props) = - if name = entityN then AList.lookup (op =) props kindN + if name = entityN then Properties.get props kindN else NONE; val defN = "def"; @@ -480,7 +481,9 @@ (* outer syntax *) val (command_keywordN, command_keyword) = markup_elem "command_keyword"; -val (commandN, command) = markup_elem "command"; + +val commandN = "command"; +val keywordN = "keyword"; val (keyword1N, keyword1) = markup_elem "keyword1"; val (keyword2N, keyword2) = markup_elem "keyword2"; val (keyword3N, keyword3) = markup_elem "keyword3"; diff -r de6cd60b1226 -r f8c4442bb3a9 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Pure/PIDE/markup.scala Fri Jun 09 11:39:02 2017 +0200 @@ -325,6 +325,7 @@ /* outer syntax */ val COMMAND = "command" + val KEYWORD = "keyword" val KEYWORD1 = "keyword1" val KEYWORD2 = "keyword2" val KEYWORD3 = "keyword3" diff -r de6cd60b1226 -r f8c4442bb3a9 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Pure/Thy/html.ML Fri Jun 09 11:39:02 2017 +0200 @@ -25,8 +25,9 @@ (* common markup *) fun span class = ("", ""); +val enclose_span = uncurry enclose o span; -val hidden = span Markup.hiddenN |-> enclose; +val hidden = enclose_span Markup.hiddenN; (* symbol output *) @@ -85,9 +86,14 @@ fun present_span symbols keywords = let + fun present_markup (name, props) = + (case Properties.get props Markup.kindN of + SOME kind => + if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I + | NONE => I) #> enclose_span name; fun present_token tok = - fold_rev (uncurry enclose o span o #1) - (Token.markups keywords tok) (output symbols (Token.unparse tok)); + fold_rev present_markup (Token.markups keywords tok) + (output symbols (Token.unparse tok)); in implode o map present_token o Command_Span.content end; diff -r de6cd60b1226 -r f8c4442bb3a9 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Pure/Thy/html.scala Fri Jun 09 11:39:02 2017 +0200 @@ -193,7 +193,8 @@ def image(src: String, alt: String = ""): XML.Elem = XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) - def source(src: String): XML.Elem = pre("source", text(src)) + def source(body: XML.Body): XML.Elem = pre("source", body) + def source(src: String): XML.Elem = source(text(src)) def style(s: String): XML.Elem = XML.elem("style", text(s)) diff -r de6cd60b1226 -r f8c4442bb3a9 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Pure/Thy/present.ML Fri Jun 09 11:39:02 2017 +0200 @@ -6,7 +6,7 @@ signature PRESENT = sig - val session_name: theory -> string + val theory_qualifier: theory -> string val document_enabled: string -> bool val document_variants: string -> (string * string) list val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> @@ -51,8 +51,6 @@ val _ = Theory.setup (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}); -val session_name = #name o Browser_Info.get; - (** global browser info state **) @@ -133,10 +131,12 @@ fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info); +val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name; + fun is_session_theory thy = (case ! session_info of NONE => false - | SOME {name, ...} => name = Resources.theory_qualifier (Context.theory_long_name thy)); + | SOME {name, ...} => name = theory_qualifier thy); (** document preparation **) diff -r de6cd60b1226 -r f8c4442bb3a9 src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Pure/Thy/present.scala Fri Jun 09 11:39:02 2017 +0200 @@ -57,7 +57,7 @@ sessions.map({ case (name, description) => (List(HTML.link(name + "/index.html", HTML.text(name))), if (description == "") Nil - else List(HTML.pre(HTML.text(description)))) }))))))) + else HTML.break ::: List(HTML.pre(HTML.text(description)))) }))))))) } def make_global_index(browser_info: Path) @@ -99,4 +99,39 @@ File.copy(font, session_fonts) } } + + + /* theory document */ + + private val document_span_elements = + Markup.Elements(Rendering.text_color.keySet + Markup.NUMERAL + Markup.COMMENT) + + def make_html(xml: XML.Body): XML.Body = + xml map { + case XML.Wrapped_Elem(markup, body1, body2) => + XML.Wrapped_Elem(markup, make_html(body1), make_html(body2)) + case XML.Elem(markup, body) => + val name = markup.name + val html = + markup.properties match { + case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => + List(HTML.span(kind, make_html(body))) + case _ => + make_html(body) + } + Rendering.text_color.get(name) match { + case Some(c) => + HTML.span(c.toString, html) + case None => + if (document_span_elements(name)) HTML.span(name, html) + else XML.Elem(markup, html) + } + case XML.Text(text) => + XML.Text(Symbol.decode(text)) + } + + def theory_document(snapshot: Document.Snapshot): XML.Body = + { + make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements)) + } } diff -r de6cd60b1226 -r f8c4442bb3a9 src/Pure/Tools/thm_deps.ML --- a/src/Pure/Tools/thm_deps.ML Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Pure/Tools/thm_deps.ML Fri Jun 09 11:39:02 2017 +0200 @@ -29,7 +29,7 @@ a :: _ => (case try (Context.get_theory thy) a of SOME thy => - (case Present.session_name thy of + (case Present.theory_qualifier thy of "" => [] | session => [session]) | NONE => []) diff -r de6cd60b1226 -r f8c4442bb3a9 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Tools/VSCode/extension/package.json Fri Jun 09 11:39:02 2017 +0200 @@ -67,8 +67,12 @@ "editor/title": [ { "when": "editorLangId == isabelle", + "command": "isabelle.preview", + "group": "navigation" + }, + { + "when": "editorLangId == isabelle", "command": "isabelle.preview-split", - "alt": "isabelle.preview", "group": "navigation" }, { diff -r de6cd60b1226 -r f8c4442bb3a9 src/Tools/VSCode/src/preview.scala --- a/src/Tools/VSCode/src/preview.scala Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Tools/VSCode/src/preview.scala Fri Jun 09 11:39:02 2017 +0200 @@ -49,7 +49,7 @@ List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))), List( HTML.chapter("Theory " + quote(model.node_name.theory_base_name)), - HTML.source(Symbol.decode(snapshot.node.commands.iterator.map(_.source).mkString))), + HTML.source(Present.theory_document(snapshot))), css = "") (label, content) } diff -r de6cd60b1226 -r f8c4442bb3a9 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Fri Jun 09 11:39:02 2017 +0200 @@ -272,11 +272,11 @@ def open_preview(view: View) { Document_Model.get(view.getBuffer) match { - case Some(model) => + case Some(model) if model.is_theory => JEdit_Editor.hyperlink_url( PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview/" + model.node_name.theory).follow(view) - case None => + case _ => } } @@ -311,7 +311,7 @@ List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css))), List( HTML.chapter("Theory " + quote(node_name.theory_base_name)), - HTML.source(snapshot.node.commands.iterator.map(_.source).mkString)), + HTML.source(Present.theory_document(snapshot))), css = "") } diff -r de6cd60b1226 -r f8c4442bb3a9 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Thu Jun 08 23:37:01 2017 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Fri Jun 09 11:39:02 2017 +0200 @@ -226,6 +226,7 @@ isabelle.newline.label=Newline with indentation of Isabelle keywords isabelle.newline.shortcut=ENTER isabelle.options.label=Isabelle options +isabelle.preview.label=HTML preview of PIDE document isabelle.reset-continuous-checking.label=Reset continuous checking isabelle.reset-font-size.label=Reset font size isabelle.reset-node-required.label=Reset node required