--- 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; }
--- 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;
--- 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 */
--- 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";
--- 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"
--- 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 = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
+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;
--- 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))
--- 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 **)
--- 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))
+ }
}
--- 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 => [])
--- 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"
},
{
--- 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)
}
--- 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 = "")
}
--- 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