# HG changeset patch # User lammich # Date 1496388364 -7200 # Node ID 10e5265c2a25ae4c15190621077d5c4cf65bb1ec # Parent 797ef48891773e5ffe0736c0c052a17209115e66# Parent c85f677cfb0a0124197edfdc6754e87ee3620098 merged diff -r 797ef4889177 -r 10e5265c2a25 etc/isabelle.css --- 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 { diff -r 797ef4889177 -r 10e5265c2a25 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- 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*) diff -r 797ef4889177 -r 10e5265c2a25 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML --- 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 diff -r 797ef4889177 -r 10e5265c2a25 src/HOL/TPTP/TPTP_Parser_Test.thy --- 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) diff -r 797ef4889177 -r 10e5265c2a25 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy --- 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) \ setup \ @@ -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)) diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/Admin/build_history.scala --- 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) } }) } diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/Admin/build_status.scala --- 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( diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/General/graphics_file.scala --- 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 diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/General/http.scala --- 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 => diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/General/path.ML --- 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))); diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/General/path.scala --- 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 diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/General/symbol.scala --- 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 diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/PIDE/xml.scala --- 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 ++= "' case XML.Text(txt) => text(txt) } body.foreach(tree) diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/Thy/html.scala --- 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 -> "_{", Symbol.bsub_decoded -> "_{",
+ Symbol.esub -> "}", Symbol.esub_decoded -> "}", + Symbol.bsup -> "^{", Symbol.bsup_decoded -> "^{",
+ Symbol.esup -> "}", Symbol.esup_decoded -> "}") + + 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 ++= "
" - case _ => s += c + def output_hidden(body: => Unit): Unit = + if (hidden) { s ++= ""; body; s ++= "" } + + 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 ++= ("") + output_hidden(output_symbol(ctrl)) + s += '<'; s ++= elem; s += '>' + output_symbol(sym) + 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 ++= "' 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)) } } diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/Thy/present.scala --- 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) diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/Thy/sessions.scala --- 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)) diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/Thy/thy_header.ML --- 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 *) diff -r 797ef4889177 -r 10e5265c2a25 src/Pure/Tools/spell_checker.scala --- 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 } diff -r 797ef4889177 -r 10e5265c2a25 src/Tools/VSCode/extension/package.json --- 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" }, diff -r 797ef4889177 -r 10e5265c2a25 src/Tools/VSCode/extension/src/preview.ts --- 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) + } } }) } diff -r 797ef4889177 -r 10e5265c2a25 src/Tools/VSCode/src/preview.scala --- 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) } } diff -r 797ef4889177 -r 10e5265c2a25 src/Tools/jEdit/src/completion_popup.scala --- 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 diff -r 797ef4889177 -r 10e5265c2a25 src/Tools/jEdit/src/symbols_dockable.scala --- 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)) diff -r 797ef4889177 -r 10e5265c2a25 src/Tools/jEdit/src/syntax_style.scala --- 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 _ => }