--- a/etc/isabelle.css Thu Jun 01 16:56:05 2017 +0200
+++ b/etc/isabelle.css Fri Jun 02 09:26:04 2017 +0200
@@ -1,22 +1,3 @@
-/* style file for Isabelle XHTML/XML output */
-
-@font-face {
- font-family: 'IsabelleText';
- src: url('fonts/IsabelleText.ttf') format('truetype');
-}
-
-@font-face {
- font-family: 'IsabelleText';
- src: url('fonts/IsabelleTextBold.ttf') format('truetype');
- font-weight: bold;
-}
-
-@font-face {
- font-family: 'Vacuous';
- src: url('fonts/Vacuous.ttf') format('truetype');
-}
-
-
/* standard document markup */
dt {
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Jun 01 16:56:05 2017 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Jun 02 09:26:04 2017 +0200
@@ -955,15 +955,13 @@
let
val config =
{cautious = cautious,
- problem_name =
- SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
- file_name))}
+ problem_name = SOME (TPTP_Problem_Name.parse_problem_name (Path.base_name file_name))}
in interpret_file' config [] path_prefixes file_name end
fun import_file cautious path_prefixes file_name type_map const_map thy =
let
val prob_name =
- TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
+ TPTP_Problem_Name.parse_problem_name (Path.base_name file_name)
val (result, thy') =
interpret_file cautious path_prefixes file_name type_map const_map thy
(*FIXME doesn't check if problem has already been interpreted*)
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Thu Jun 01 16:56:05 2017 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Fri Jun 02 09:26:04 2017 +0200
@@ -1790,8 +1790,7 @@
(on_load : proof_annotation -> theory -> (proof_annotation * theory)) thy =
let
val prob_name =
- Path.base file_name
- |> Path.implode
+ Path.base_name file_name
|> TPTP_Problem_Name.parse_problem_name
val thy1 = TPTP_Interpret.import_file cautious path_prefixes file_name [] [] thy
val fms = get_fmlas_of_prob thy1 prob_name
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy Thu Jun 01 16:56:05 2017 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy Fri Jun 02 09:26:04 2017 +0200
@@ -47,8 +47,7 @@
(*test against all TPTP problems*)
fun problem_names () =
- map (Path.base #>
- Path.implode #>
+ map (Path.base_name #>
TPTP_Problem_Name.parse_problem_name #>
TPTP_Problem_Name.mangle_problem_name)
(TPTP_Syntax.get_file_list tptp_probs_dir)
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Thu Jun 01 16:56:05 2017 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Fri Jun 02 09:26:04 2017 +0200
@@ -58,7 +58,7 @@
val prob_names =
probs
- |> map (Path.base #> Path.implode #> TPTP_Problem_Name.Nonstandard)
+ |> map (Path.base_name #> TPTP_Problem_Name.Nonstandard)
\<close>
setup \<open>
@@ -575,7 +575,9 @@
fun test_partial_reconstruction thy prob_file =
let
val prob_name =
- (Path.base #> Path.implode #> TPTP_Problem_Name.Nonstandard) prob_file
+ prob_file
+ |> Path.base_name
+ |> TPTP_Problem_Name.Nonstandard
val thy' =
try
@@ -658,8 +660,7 @@
val ctxt = Proof_Context.init_global thy' (*FIXME pass ctxt instead of thy*)
val prob_name =
file
- |> Path.base
- |> Path.implode
+ |> Path.base_name
|> TPTP_Problem_Name.Nonstandard
in
Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
--- a/src/Pure/Admin/build_history.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/Admin/build_history.scala Fri Jun 02 09:26:04 2017 +0200
@@ -211,7 +211,7 @@
val build_end = Date.now()
val build_info: Build_Log.Build_Info =
- Build_Log.Log_File(log_path.base.implode, build_result.out_lines).
+ Build_Log.Log_File(log_path.base_name, build_result.out_lines).
parse_build_info(ml_statistics = true)
@@ -489,7 +489,7 @@
val log = Path.explode(line)
val bytes = ssh.read_bytes(log)
ssh.rm(log)
- (log.base.implode, bytes)
+ (log.base_name, bytes)
}
})
}
--- a/src/Pure/Admin/build_status.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Fri Jun 02 09:26:04 2017 +0200
@@ -273,7 +273,7 @@
case Nil => Nil
case sessions =>
HTML.break :::
- List(HTML.error_message(HTML.span(HTML.text("Failed sessions:")))) :::
+ List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) :::
List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
})
}))))))
@@ -416,7 +416,7 @@
HTML.text(" (" + session.head.timing.message_resources + ")"))))) ::
data_entry.sessions.flatMap(session =>
List(
- HTML.id("session_" + session.name)(HTML.section(session.name)),
+ HTML.section(HTML.id("session_" + session.name), session.name),
HTML.par(
HTML.description(
List(
--- a/src/Pure/General/graphics_file.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/General/graphics_file.scala Fri Jun 02 09:26:04 2017 +0200
@@ -46,7 +46,7 @@
val mapper = new DefaultFontMapper
for {
font <- Isabelle_System.fonts()
- name <- Library.try_unsuffix(".ttf", font.base.implode)
+ name <- Library.try_unsuffix(".ttf", font.base_name)
} {
val parameters = new DefaultFontMapper.BaseFontParameters(File.platform_path(font))
parameters.encoding = BaseFont.IDENTITY_H
--- a/src/Pure/General/http.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/General/http.scala Fri Jun 02 09:26:04 2017 +0200
@@ -137,7 +137,7 @@
private lazy val html_fonts: SortedMap[String, Bytes] =
SortedMap(
- Isabelle_System.fonts(html = true).map(path => (path.base.implode -> Bytes.read(path))): _*)
+ Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
def fonts(root: String = "/fonts"): Handler =
get(root, uri =>
--- a/src/Pure/General/path.ML Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/General/path.ML Fri Jun 02 09:26:04 2017 +0200
@@ -29,6 +29,7 @@
val print: T -> string
val dir: T -> T
val base: T -> T
+ val base_name: T -> string
val ext: string -> T -> T
val split_ext: T -> T * string
val expand: T -> T
@@ -183,6 +184,7 @@
val dir = split_path #1;
val base = split_path (fn (_, s) => Path [Basic s]);
+val base_name = implode_path o base;
fun ext "" = I
| ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
--- a/src/Pure/General/path.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/General/path.scala Fri Jun 02 09:26:04 2017 +0200
@@ -149,6 +149,7 @@
def dir: Path = split_path._1
def base: Path = new Path(List(Path.Basic(split_path._2)))
+ def base_name: String = base.implode
def ext(e: String): Path =
if (e == "") this
--- a/src/Pure/General/symbol.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/General/symbol.scala Fri Jun 02 09:26:04 2017 +0200
@@ -487,10 +487,10 @@
val sup_decoded = decode(sup)
val bold_decoded = decode(bold)
val emph_decoded = decode(emph)
- val bsub_decoded = decode("\\<^bsub>")
- val esub_decoded = decode("\\<^esub>")
- val bsup_decoded = decode("\\<^bsup>")
- val esup_decoded = decode("\\<^esup>")
+ val bsub_decoded = decode(bsub)
+ val esub_decoded = decode(esub)
+ val bsup_decoded = decode(bsup)
+ val esup_decoded = decode(esup)
}
@@ -585,6 +585,10 @@
val sup = "\\<^sup>"
val bold = "\\<^bold>"
val emph = "\\<^emph>"
+ val bsub = "\\<^bsub>"
+ val esub = "\\<^esub>"
+ val bsup = "\\<^bsup>"
+ val esup = "\\<^esup>"
def sub_decoded: Symbol = symbols.sub_decoded
def sup_decoded: Symbol = symbols.sup_decoded
--- a/src/Pure/PIDE/xml.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/PIDE/xml.scala Fri Jun 02 09:26:04 2017 +0200
@@ -93,33 +93,44 @@
/** string representation **/
+ def output_char(c: Char, s: StringBuilder)
+ {
+ c match {
+ case '<' => s ++= "<"
+ case '>' => s ++= ">"
+ case '&' => s ++= "&"
+ case '"' => s ++= """
+ case '\'' => s ++= "'"
+ case _ => s += c
+ }
+ }
+
+ def output_string(str: String, s: StringBuilder)
+ {
+ if (str == null) s ++= str
+ else str.iterator.foreach(c => output_char(c, s))
+ }
+
def string_of_body(body: Body): String =
{
val s = new StringBuilder
- def text(txt: String) {
- if (txt == null) s ++= txt
- else {
- for (c <- txt.iterator) c match {
- case '<' => s ++= "<"
- case '>' => s ++= ">"
- case '&' => s ++= "&"
- case '"' => s ++= """
- case '\'' => s ++= "'"
- case _ => s += c
- }
+ def text(txt: String) { output_string(txt, s) }
+ def elem(markup: Markup)
+ {
+ s ++= markup.name
+ for ((a, b) <- markup.properties) {
+ s += ' '; s ++= a; s += '='; s += '"'; text(b); s += '"'
}
}
- def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
- def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
def tree(t: Tree): Unit =
t match {
case XML.Elem(markup, Nil) =>
- s ++= "<"; elem(markup); s ++= "/>"
+ s += '<'; elem(markup); s ++= "/>"
case XML.Elem(markup, ts) =>
- s ++= "<"; elem(markup); s ++= ">"
+ s += '<'; elem(markup); s += '>'
ts.foreach(tree)
- s ++= "</"; s ++= markup.name; s ++= ">"
+ s ++= "</"; s ++= markup.name; s += '>'
case XML.Text(txt) => text(txt)
}
body.foreach(tree)
--- a/src/Pure/Thy/html.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/Thy/html.scala Fri Jun 02 09:26:04 2017 +0200
@@ -9,51 +9,61 @@
object HTML
{
- /* encode text with control symbols */
+ /* output text with control symbols */
- val control =
+ private val control =
Map(
- Symbol.sub -> "sub",
- Symbol.sub_decoded -> "sub",
- Symbol.sup -> "sup",
- Symbol.sup_decoded -> "sup",
- Symbol.bold -> "b",
- Symbol.bold_decoded -> "b")
+ Symbol.sub -> "sub", Symbol.sub_decoded -> "sub",
+ Symbol.sup -> "sup", Symbol.sup_decoded -> "sup",
+ Symbol.bold -> "b", Symbol.bold_decoded -> "b")
+
+ private val control_block =
+ Map(
+ Symbol.bsub -> "<sub>", Symbol.bsub_decoded -> "<sub>",
+ Symbol.esub -> "</sub>", Symbol.esub_decoded -> "</sub>",
+ Symbol.bsup -> "<sup>", Symbol.bsup_decoded -> "<sup>",
+ Symbol.esup -> "</sup>", Symbol.esup_decoded -> "</sup>")
+
+ def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
- def output(text: String, s: StringBuilder)
+ def output(text: String, s: StringBuilder, hidden: Boolean)
{
- def output_char(c: Char) =
- c match {
- case '<' => s ++= "<"
- case '>' => s ++= ">"
- case '&' => s ++= "&"
- case '"' => s ++= """
- case '\'' => s ++= "'"
- case '\n' => s ++= "<br/>"
- case _ => s += c
+ def output_hidden(body: => Unit): Unit =
+ if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
+
+ def output_symbol(sym: Symbol.Symbol): Unit =
+ if (sym != "") {
+ control_block.get(sym) match {
+ case Some(html) if html.startsWith("</") =>
+ s ++= html; output_hidden(XML.output_string(sym, s))
+ case Some(html) =>
+ output_hidden(XML.output_string(sym, s)); s ++= html
+ case None =>
+ XML.output_string(sym, s)
+ }
}
- def output_chars(str: String) = str.iterator.foreach(output_char(_))
var ctrl = ""
for (sym <- Symbol.iterator(text)) {
- if (control.isDefinedAt(sym)) ctrl = sym
+ if (is_control(sym)) { output_symbol(ctrl); ctrl = sym }
else {
control.get(ctrl) match {
case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
- s ++= ("<" + elem + ">")
- output_chars(sym)
- s ++= ("</" + elem + ">")
+ output_hidden(output_symbol(ctrl))
+ s += '<'; s ++= elem; s += '>'
+ output_symbol(sym)
+ s ++= "</"; s ++= elem; s += '>'
case _ =>
- output_chars(ctrl)
- output_chars(sym)
+ output_symbol(ctrl)
+ output_symbol(sym)
}
ctrl = ""
}
}
- output_chars(ctrl)
+ output_symbol(ctrl)
}
- def output(text: String): String = Library.make_string(output(text, _))
+ def output(text: String): String = Library.make_string(output(text, _, hidden = false))
/* output XML as HTML */
@@ -62,41 +72,51 @@
Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
"ul", "ol", "dl", "li", "dt", "dd")
- def output(body: XML.Body, s: StringBuilder)
+ def output(body: XML.Body, s: StringBuilder, hidden: Boolean)
{
- def attrib(p: (String, String)): Unit =
- { s ++= " "; s ++= p._1; s ++= "=\""; output(p._2, s); s ++= "\"" }
- def elem(markup: Markup): Unit =
- { s ++= markup.name; markup.properties.foreach(attrib) }
+ def elem(markup: Markup)
+ {
+ s ++= markup.name
+ for ((a, b) <- markup.properties) {
+ s += ' '; s ++= a; s += '='; s += '"'; output(b, s, hidden); s += '"'
+ }
+ }
def tree(t: XML.Tree): Unit =
t match {
case XML.Elem(markup, Nil) =>
- s ++= "<"; elem(markup); s ++= "/>"
+ s += '<'; elem(markup); s ++= "/>"
case XML.Elem(markup, ts) =>
if (structural_elements(markup.name)) s += '\n'
- s ++= "<"; elem(markup); s ++= ">"
+ s += '<'; elem(markup); s += '>'
ts.foreach(tree)
- s ++= "</"; s ++= markup.name; s ++= ">"
+ s ++= "</"; s ++= markup.name; s += '>'
if (structural_elements(markup.name)) s += '\n'
- case XML.Text(txt) => output(txt, s)
+ case XML.Text(txt) =>
+ output(txt, s, hidden)
}
body.foreach(tree)
}
- def output(body: XML.Body): String = Library.make_string(output(body, _))
- def output(tree: XML.Tree): String = output(List(tree))
+ def output(body: XML.Body, hidden: Boolean): String =
+ Library.make_string(output(body, _, hidden))
+
+ def output(tree: XML.Tree, hidden: Boolean): String =
+ output(List(tree), hidden)
/* attributes */
- class Attribute(name: String, value: String)
- { def apply(elem: XML.Elem): XML.Elem = elem + (name -> value) }
+ class Attribute(val name: String, value: String)
+ {
+ def xml: XML.Attribute = name -> value
+ def apply(elem: XML.Elem): XML.Elem = elem + xml
+ }
- def id(s: String) = new Attribute("id", s)
- def css_class(name: String) = new Attribute("class", name)
+ def id(s: String): Attribute = new Attribute("id", s)
+ def class_(name: String): Attribute = new Attribute("class", name)
- def width(w: Int) = new Attribute("width", w.toString)
- def height(h: Int) = new Attribute("height", h.toString)
+ def width(w: Int): Attribute = new Attribute("width", w.toString)
+ def height(h: Int): Attribute = new Attribute("height", h.toString)
def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
@@ -105,11 +125,19 @@
def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
val break: XML.Body = List(XML.elem("br"))
- class Operator(name: String)
- { def apply(body: XML.Body): XML.Elem = XML.elem(name, body) }
+ class Operator(val name: String)
+ {
+ def apply(body: XML.Body): XML.Elem = XML.elem(name, body)
+ def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body))
+ def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body)
+ }
class Heading(name: String) extends Operator(name)
- { def apply(txt: String): XML.Elem = super.apply(text(txt)) }
+ {
+ def apply(txt: String): XML.Elem = super.apply(text(txt))
+ def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt))
+ def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt))
+ }
val div = new Operator("div")
val span = new Operator("span")
@@ -142,28 +170,31 @@
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 = css_class("source")(div(List(pre(text(src)))))
+ def source(src: String): XML.Elem = pre("source", text(src))
def style(s: String): XML.Elem = XML.elem("style", text(s))
+ def style_file(href: String): XML.Elem =
+ XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
+
/* messages */
// background
- val writeln_message: Attribute = css_class("writeln_message")
- val warning_message: Attribute = css_class("warning_message")
- val error_message: Attribute = css_class("error_message")
+ val writeln_message: Attribute = class_("writeln_message")
+ val warning_message: Attribute = class_("warning_message")
+ val error_message: Attribute = class_("error_message")
// underline
- val writeln: Attribute = css_class("writeln")
- val warning: Attribute = css_class("warning")
- val error: Attribute = css_class("error")
+ val writeln: Attribute = class_("writeln")
+ val warning: Attribute = class_("warning")
+ val error: Attribute = class_("error")
/* tooltips */
def tooltip(item: XML.Body, tip: XML.Body): XML.Elem =
- span(item ::: List(css_class("tooltip")(div(tip))))
+ span(item ::: List(div("tooltip", tip)))
def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem =
HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
@@ -180,28 +211,66 @@
XML.Elem(Markup("meta",
List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
- def head_css(css: String): XML.Elem =
- XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil)
-
- def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String =
+ def output_document(head: XML.Body, body: XML.Body,
+ css: String = "isabelle.css", hidden: Boolean = true): String =
+ {
cat_lines(
List(header,
- output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)),
- output(XML.elem("body", body))))
+ output(
+ XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head),
+ hidden = hidden),
+ output(XML.elem("body", body), hidden = hidden)))
+ }
+
+
+ /* fonts */
+
+ def fonts_url(): String => String =
+ (for (font <- Isabelle_System.fonts(html = true))
+ yield (font.base_name -> Url.print_file(font.file))).toMap
+
+ def fonts_dir(prefix: String)(ttf_name: String): String =
+ prefix + "/" + ttf_name
+
+ def fonts_css(make_url: String => String = fonts_url()): String =
+ {
+ def font_face(name: String, ttf_name: String, bold: Boolean = false): String =
+ cat_lines(
+ List(
+ "@font-face {",
+ " font-family: '" + name + "';",
+ " src: url('" + make_url(ttf_name) + "') format('truetype');") :::
+ (if (bold) List(" font-weight: bold;") else Nil) :::
+ List("}"))
+
+ List(
+ "/* Isabelle fonts */",
+ font_face("IsabelleText", "IsabelleText.ttf"),
+ font_face("IsabelleText", "IsabelleTextBold.ttf", bold = true),
+ font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n")
+ }
/* document directory */
+ def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
+
+ def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts"))
+ {
+ File.write(dir + isabelle_css.base,
+ fonts_css(make_url) + "\n\n\n" + File.read(isabelle_css))
+ }
+
def init_dir(dir: Path)
{
Isabelle_System.mkdirs(dir)
- File.copy(Path.explode("~~/etc/isabelle.css"), dir)
+ write_isabelle_css(dir)
}
def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
- css: String = "isabelle.css")
+ css: String = isabelle_css.base_name, hidden: Boolean = true)
{
init_dir(dir)
- File.write(dir + Path.basic(name), output_document(head, body, css))
+ File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden))
}
}
--- a/src/Pure/Thy/present.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/Thy/present.scala Fri Jun 02 09:26:04 2017 +0200
@@ -52,12 +52,12 @@
HTML.chapter(title) ::
(if (sessions.isEmpty) Nil
else
- List(HTML.css_class("sessions")(HTML.div(List(
- HTML.description(
+ List(HTML.div("sessions",
+ List(HTML.description(
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 List(HTML.pre(HTML.text(description)))) })))))))
}
def make_global_index(browser_info: Path)
@@ -93,7 +93,7 @@
File.copy(graph_file, session_graph.file)
Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph))
- File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix)
+ HTML.write_isabelle_css(session_prefix)
for (font <- Isabelle_System.fonts(html = true))
File.copy(font, session_fonts)
--- a/src/Pure/Thy/sessions.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Jun 02 09:26:04 2017 +0200
@@ -574,7 +574,7 @@
val global_theories =
for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
yield {
- val thy_name = Path.explode(thy).expand.base.implode
+ val thy_name = Path.explode(thy).expand.base_name
if (Long_Name.is_qualified(thy_name))
error("Bad qualified name for global theory " +
quote(thy_name) + Position.here(pos))
--- a/src/Pure/Thy/thy_header.ML Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/Thy/thy_header.ML Fri Jun 02 09:26:04 2017 +0200
@@ -114,7 +114,7 @@
val ml_roots = ["ML_Root0", "ML_Root"];
val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
-val import_name = Path.implode o Path.base o Path.explode;
+val import_name = Path.base_name o Path.explode;
(* header args *)
--- a/src/Pure/Tools/spell_checker.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Pure/Tools/spell_checker.scala Fri Jun 02 09:26:04 2017 +0200
@@ -57,7 +57,7 @@
class Dictionary private[Spell_Checker](val path: Path)
{
- val lang = path.split_ext._1.base.implode
+ val lang = path.split_ext._1.base_name
val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
override def toString: String = lang
}
--- a/src/Tools/VSCode/extension/package.json Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Tools/VSCode/extension/package.json Fri Jun 02 09:26:04 2017 +0200
@@ -10,7 +10,7 @@
"document preparation"
],
"icon": "isabelle.png",
- "version": "0.12.0",
+ "version": "0.13.0",
"publisher": "makarius",
"license": "MIT",
"repository": { "url": "http://isabelle.in.tum.de/repos/isabelle" },
--- a/src/Tools/VSCode/extension/src/preview.ts Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts Fri Jun 02 09:26:04 2017 +0200
@@ -79,8 +79,10 @@
const preview_uri = encode_preview(Uri.parse(params.uri))
if (preview_uri) {
preview_content.set(preview_uri.toString(), params.content)
- if (params.column == 0) content_provider.update(preview_uri)
- else commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
+ content_provider.update(preview_uri)
+ if (params.column != 0) {
+ commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
+ }
}
})
}
--- a/src/Tools/VSCode/src/preview.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Tools/VSCode/src/preview.scala Fri Jun 02 09:26:04 2017 +0200
@@ -45,14 +45,12 @@
{
val label = "Preview " + quote(model.node_name.toString)
val content =
- HTML.output_document(head = Nil, css = "", body =
+ HTML.output_document(
+ List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
List(
- HTML.chapter(label),
- HTML.itemize(
- snapshot.node.commands.toList.flatMap(
- command =>
- if (command.span.name == "") None
- else Some(HTML.text(command.span.name))))))
+ HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
+ HTML.source(Symbol.decode(snapshot.node.commands.iterator.map(_.source).mkString))),
+ css = "")
(label, content)
}
}
--- a/src/Tools/jEdit/src/completion_popup.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Jun 02 09:26:04 2017 +0200
@@ -193,7 +193,7 @@
val path = Path.explode(text)
val (dir, base_name) =
if (text == "" || text.endsWith("/")) (path, "")
- else (path.dir, path.base.implode)
+ else (path.dir, path.base_name)
val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir))
val files = directory.listFiles
--- a/src/Tools/jEdit/src/symbols_dockable.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Fri Jun 02 09:26:04 2017 +0200
@@ -96,7 +96,7 @@
action =
Action(Symbol.decode(symbol)) {
val text_area = view.getTextArea
- if (is_control && HTML.control.isDefinedAt(symbol))
+ if (is_control && HTML.is_control(symbol))
Syntax_Style.edit_control_style(text_area, symbol)
else
text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
--- a/src/Tools/jEdit/src/syntax_style.scala Thu Jun 01 16:56:05 2017 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala Fri Jun 02 09:26:04 2017 +0200
@@ -138,7 +138,7 @@
def update_style(text: String): String =
{
val result = new StringBuilder
- for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) {
+ for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) {
if (Symbol.is_controllable(sym)) result ++= control_decoded
result ++= sym
}
@@ -148,7 +148,7 @@
text_area.getSelection.foreach(sel => {
val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
JEdit_Lib.try_get_text(buffer, before) match {
- case Some(s) if HTML.control.isDefinedAt(s) =>
+ case Some(s) if HTML.is_control(s) =>
text_area.extendSelection(before.start, before.stop)
case _ =>
}