--- a/Admin/Release/CHECKLIST Fri Dec 22 21:00:07 2017 +0000
+++ b/Admin/Release/CHECKLIST Fri Dec 22 21:01:53 2017 +0000
@@ -5,8 +5,6 @@
- check Admin/components;
-- test 'display_drafts' command;
-
- test Isabelle/jEdit: print buffer
- test "#!/usr/bin/env isabelle_scala_script";
--- a/Admin/components/components.sha1 Fri Dec 22 21:00:07 2017 +0000
+++ b/Admin/components/components.sha1 Fri Dec 22 21:01:53 2017 +0000
@@ -63,6 +63,7 @@
8ff0eedf0191d808ecc58c6b3149a4697f29ab21 isabelle_fonts-20160812-1.tar.gz
9283e3b0b4c7239f57b18e076ec8bb21021832cb isabelle_fonts-20160812.tar.gz
620cffeb125e198b91a716da116f754d6cc8174b isabelle_fonts-20160830.tar.gz
+b70690c85c05d0ca5bc29287abd20142f6ddcfb0 isabelle_fonts-20171222.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
--- a/Admin/components/main Fri Dec 22 21:00:07 2017 +0000
+++ b/Admin/components/main Fri Dec 22 21:01:53 2017 +0000
@@ -4,7 +4,7 @@
csdp-6.x
cvc4-1.5-3
e-2.0-1
-isabelle_fonts-20160830
+isabelle_fonts-20171222
jdk-8u152
jedit_build-20170319
jfreechart-1.0.14-1
--- a/NEWS Fri Dec 22 21:00:07 2017 +0000
+++ b/NEWS Fri Dec 22 21:01:53 2017 +0000
@@ -41,8 +41,11 @@
isabelle build -D '~~/src/ZF'
-
-*** Prover IDE -- Isabelle/Scala/jEdit ***
+* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
+use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
+
+
+*** Isabelle/jEdit Prover IDE ***
* PIDE markup for session ROOT files: allows to complete session names,
follow links to theories and document files etc.
@@ -71,8 +74,16 @@
arguments into this format.
* Action "isabelle.preview" is able to present more file formats,
-notably bibtex database files and plain text files.
-
+notably bibtex database files and ML files.
+
+* Action "isabelle.draft" is similar to "isabelle.preview", but shows a
+plain-text document draft.
+
+
+*** Isabelle/VSCode Prover IDE ***
+
+* HTML preview of theories and other file-formats similar to
+Isabelle/jEdit.
*** Document preparation ***
--- a/etc/isabelle.css Fri Dec 22 21:00:07 2017 +0000
+++ b/etc/isabelle.css Fri Dec 22 21:01:53 2017 +0000
@@ -31,6 +31,7 @@
/* basic syntax markup */
.hidden { font-family: Vacuous; font-size: 1%; color: rgba(255,255,255,0); }
+.control { font-weight: bold; font-style: italic; }
.binding { color: #336655; }
.tfree { color: #A020F0; }
--- a/lib/Tools/latex Fri Dec 22 21:00:07 2017 +0000
+++ b/lib/Tools/latex Fri Dec 22 21:01:53 2017 +0000
@@ -13,7 +13,7 @@
echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
echo
echo " Options are:"
- echo " -o FORMAT specify output format: pdf (default), dvi, bbl, idx, sty, syms"
+ echo " -o FORMAT specify output format: pdf (default), dvi, bbl, idx, sty"
echo
echo " Run LaTeX (and related tools) on FILE (default root.tex),"
echo " producing the specified output format."
@@ -83,16 +83,6 @@
done
}
-function extract_syms ()
-{
- perl -n \
- -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
- "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
- perl -n \
- -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
- "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
-}
-
case "$OUTFORMAT" in
pdf)
check_root && \
@@ -118,10 +108,6 @@
copy_styles
RC="$?"
;;
- syms)
- extract_syms
- RC="$?"
- ;;
*)
fail "Bad output format '$OUTFORMAT'"
;;
--- a/lib/fonts/Vacuous.sfd Fri Dec 22 21:00:07 2017 +0000
+++ b/lib/fonts/Vacuous.sfd Fri Dec 22 21:01:53 2017 +0000
@@ -20,7 +20,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1471028867
-ModificationTime: 1471030389
+ModificationTime: 1513953645
PfmFamily: 17
TTFWeight: 500
TTFWidth: 5
@@ -49,11 +49,11 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 8560 20 14
+WinInfo: 0 20 14
BeginPrivate: 0
EndPrivate
TeXData: 1 0 0 346030 173015 115343 0 1048576 115343 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144
-BeginChars: 1114112 7
+BeginChars: 1114112 11
StartChar: uni2759
Encoding: 10073 10073 0
@@ -194,5 +194,85 @@
32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
EndSplineSet
EndChar
+
+StartChar: backslash
+Encoding: 92 92 7
+Width: 44
+VWidth: 1670
+Flags: HW
+LayerCount: 2
+Fore
+SplineSet
+33.4502 5 m 128
+ 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
+ 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
+ 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
+ 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
+ 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
+ 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
+ 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
+ 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
+EndSplineSet
+EndChar
+
+StartChar: less
+Encoding: 60 60 8
+Width: 44
+VWidth: 1670
+Flags: HW
+LayerCount: 2
+Fore
+SplineSet
+33.4502 5 m 128
+ 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
+ 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
+ 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
+ 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
+ 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
+ 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
+ 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
+ 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
+EndSplineSet
+EndChar
+
+StartChar: greater
+Encoding: 62 62 9
+Width: 44
+VWidth: 1670
+Flags: HW
+LayerCount: 2
+Fore
+SplineSet
+33.4502 5 m 128
+ 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
+ 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
+ 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
+ 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
+ 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
+ 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
+ 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
+ 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
+EndSplineSet
+EndChar
+
+StartChar: asciicircum
+Encoding: 94 94 10
+Width: 44
+VWidth: 1670
+Flags: HW
+LayerCount: 2
+Fore
+SplineSet
+33.4502 5 m 128
+ 33.4502 1.7998 32.2998 -0.966797 30 -3.2998 c 128
+ 27.7002 -5.63379 24.9336 -6.7998 21.7002 -6.7998 c 128
+ 18.4668 -6.7998 15.7002 -5.63379 13.4004 -3.2998 c 128
+ 11.1006 -0.966797 9.9502 1.7998 9.9502 5 c 128
+ 9.9502 8.2002 11.1006 10.9668 13.4004 13.2998 c 128
+ 15.7002 15.6328 18.4668 16.7998 21.7002 16.7998 c 128
+ 24.9336 16.7998 27.7002 15.6328 30 13.2998 c 128
+ 32.2998 10.9668 33.4502 8.2002 33.4502 5 c 128
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/lib/texinputs/draft.tex Fri Dec 22 21:00:07 2017 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-%%
-%% root for draft documents
-%%
-
-\documentclass[10pt,a4paper]{article}
-\usepackage{isabelle,isabellesym,pdfsetup}
-
-%packages for unusual symbols according to 'isabelle latex -o syms'
-\usepackage{amssymb}
-\usepackage{textcomp}
-
-\pagestyle{myheadings}
-\newcommand{\isamarkupfile}[1]%
-{{\def\isacharunderscore{\mbox{-}}%
-\section*{#1}\markright{FILE~``\isabellecontext''}}}
-
-\begin{document}
-\input{session}
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Dec 22 21:01:53 2017 +0000
@@ -613,21 +613,4 @@
@{rail \<open>A + sep\<close>}
\<close>
-
-section \<open>Draft presentation\<close>
-
-text \<open>
- \begin{matharray}{rcl}
- @{command_def "display_drafts"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
- \end{matharray}
-
- @{rail \<open>
- @@{command display_drafts} (@{syntax name} +)
- \<close>}
-
- \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a given list
- of raw source files. Only those symbols that do not require additional
- {\LaTeX} packages are displayed properly, everything else is left verbatim.
-\<close>
-
end
--- a/src/Doc/JEdit/JEdit.thy Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Doc/JEdit/JEdit.thy Fri Dec 22 21:01:53 2017 +0000
@@ -1902,6 +1902,9 @@
current document node in the default web browser. The content is derived
from the semantic markup produced by the prover, and thus depends on the
status of formal processing.
+
+ Action @{action_def isabelle.draft} is similar to @{action
+ isabelle.preview}, but shows a plain-text document draft.
\<close>
--- a/src/Doc/System/Presentation.thy Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Doc/System/Presentation.thy Fri Dec 22 21:01:53 2017 +0000
@@ -254,8 +254,7 @@
\<open>Usage: isabelle latex [OPTIONS] [FILE]
Options are:
- -o FORMAT specify output format: pdf (default), dvi,
- bbl, idx, sty, syms
+ -o FORMAT specify output format: pdf (default), dvi, bbl, idx, sty
Run LaTeX (and related tools) on FILE (default root.tex),
producing the specified output format.\<close>}
@@ -269,9 +268,6 @@
The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
the distribution. This is useful in special situations where the document
sources are to be processed another time by separate tools.
-
- The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists of symbols that
- are available without loading additional {\LaTeX} packages.
\<close>
--- a/src/Pure/General/symbol.scala Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Pure/General/symbol.scala Fri Dec 22 21:01:53 2017 +0000
@@ -583,6 +583,11 @@
val control_prefix = "\\<^"
val control_suffix = ">"
+ def control_name(sym: Symbol): Option[String] =
+ if (is_control_encoded(sym))
+ Some(sym.substring(control_prefix.length, sym.length - control_suffix.length))
+ else None
+
def is_control_encoded(sym: Symbol): Boolean =
sym.startsWith(control_prefix) && sym.endsWith(control_suffix)
--- a/src/Pure/PIDE/document.scala Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Pure/PIDE/document.scala Fri Dec 22 21:01:53 2017 +0000
@@ -45,7 +45,7 @@
/* document blobs: auxiliary files */
- sealed case class Blob(bytes: Bytes, chunk: Symbol.Text_Chunk, changed: Boolean)
+ sealed case class Blob(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean)
{
def unchanged: Blob = copy(changed = false)
}
@@ -323,9 +323,9 @@
def command_start(cmd: Command): Option[Text.Offset] =
Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
- def get_text: String =
+ def source: String =
get_blob match {
- case Some(blob) => blob.bytes.text
+ case Some(blob) => blob.source
case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString
}
}
@@ -821,17 +821,36 @@
def markup_to_XML(
version: Version,
- node: Node,
+ node_name: Node.Name,
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).iterator
- } yield tree).toList
+ val node = version.nodes(node_name)
+ if (node_name.is_theory) {
+ val markup_index = Command.Markup_Index.markup
+ (for {
+ command <- node.commands.iterator
+ command_range <- command.range.try_restrict(range).iterator
+ markup = command_markup(version, command, markup_index, command_range, elements)
+ tree <- markup.to_XML(command_range, command.source, elements).iterator
+ } yield tree).toList
+ }
+ else {
+ val node_source = node.source
+ Text.Range(0, node_source.length).try_restrict(range) match {
+ case None => Nil
+ case Some(node_range) =>
+ val markup =
+ version.nodes.commands_loading(node_name).headOption match {
+ case None => Markup_Tree.empty
+ case Some(command) =>
+ val chunk_name = Symbol.Text_Chunk.File(node_name.node)
+ val markup_index = Command.Markup_Index(false, chunk_name)
+ command_markup(version, command, markup_index, node_range, elements)
+ }
+ markup.to_XML(node_range, node_source, elements)
+ }
+ }
}
def node_consolidated(version: Version, name: Node.Name): Boolean =
@@ -910,7 +929,7 @@
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)
+ state.markup_to_XML(version, node_name, range, elements)
/* find command */
--- a/src/Pure/Pure.thy Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Pure/Pure.thy Fri Dec 22 21:01:53 2017 +0000
@@ -84,7 +84,7 @@
"locale_deps" "class_deps" "thm_deps" "print_term_bindings"
"print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
"prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
- and "display_drafts" "print_state" :: diag
+ and "print_state" :: diag
and "welcome" :: diag
and "end" :: thy_end % "theory"
and "realizers" :: thy_decl
@@ -1208,12 +1208,6 @@
Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"
(Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
-val _ =
- Outer_Syntax.command \<^command_keyword>\<open>display_drafts\<close>
- "display raw source files with symbols"
- (Scan.repeat1 Parse.path >> (fn names =>
- Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
-
in end\<close>
--- a/src/Pure/Thy/html.scala Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Pure/Thy/html.scala Fri Dec 22 21:01:53 2017 +0000
@@ -56,7 +56,14 @@
case Some(html) =>
output_hidden(output_string(sym)); s ++= html
case None =>
- output_string(sym)
+ if (hidden && Symbol.is_control_encoded(sym)) {
+ output_hidden(output_string(Symbol.control_prefix))
+ s ++= "<span class=\"control\">"
+ output_string(Symbol.control_name(sym).get)
+ s ++= "</span>"
+ output_hidden(output_string(Symbol.control_suffix))
+ }
+ else output_string(sym)
}
}
--- a/src/Pure/Thy/latex.ML Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Pure/Thy/latex.ML Fri Dec 22 21:01:53 2017 +0000
@@ -18,8 +18,6 @@
val latex_control: Symbol.symbol
val is_latex_control: Symbol.symbol -> bool
val embed_raw: string -> string
- val output_known_symbols: (string -> bool) * (string -> bool) ->
- Symbol.symbol list -> string
val output_symbols: Symbol.symbol list -> string
val output_syms: string -> string
val output_token: Token.T -> string
@@ -30,8 +28,6 @@
val environment_block: string -> text list -> text
val environment: string -> string -> string
val isabelle_body: string -> text list -> text list
- val symbol_source: (string -> bool) * (string -> bool) ->
- string -> Symbol.symbol list -> string
val theory_entry: string -> string
val latexN: string
end;
@@ -169,14 +165,12 @@
SOME s => s
| NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
-val output_chrs = translate_string output_chr;
-
-fun output_known_sym (known_sym, known_ctrl) sym =
+fun output_sym sym =
(case Symbol.decode sym of
Symbol.Char s => output_chr s
| Symbol.UTF8 s => s
- | Symbol.Sym s => if known_sym s then enclose_name "{\\isasym" "}" s else output_chrs sym
- | Symbol.Control s => if known_ctrl s then enclose_name "\\isactrl" " " s else output_chrs sym
+ | Symbol.Sym s => enclose_name "{\\isasym" "}" s
+ | Symbol.Control s => enclose_name "\\isactrl" " " s
| Symbol.Malformed s => error (Symbol.malformed_msg s)
| Symbol.EOF => error "Bad EOF symbol");
@@ -186,10 +180,10 @@
Scan.one (is_latex_control o Symbol_Pos.symbol) --
Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
-fun scan_latex known =
+val scan_latex =
Scan.one (is_latex_control o Symbol_Pos.symbol) |--
Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) ||
- Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol);
+ Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol);
fun read scan syms =
Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
@@ -199,14 +193,13 @@
fun length_symbols syms =
fold Integer.add (these (read scan_latex_length syms)) 0;
-fun output_known_symbols known syms =
+fun output_symbols syms =
if exists is_latex_control syms then
- (case read (scan_latex known) syms of
+ (case read scan_latex syms of
SOME ss => implode ss
| NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
- else implode (map (output_known_sym known) syms);
+ else implode (map output_sym syms);
-val output_symbols = output_known_symbols (K true, K true);
val output_syms = output_symbols o Symbol.explode;
val output_syms_antiq =
@@ -265,16 +258,10 @@
fun environment_block name = environment_delim name |-> enclose_body #> block;
fun environment name = environment_delim name |-> enclose;
-fun isabelle_body_delim name =
- ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n",
- "%\n\\end{isabellebody}%\n");
-
-fun isabelle_body name = isabelle_body_delim name |-> enclose_body;
-
-fun symbol_source known name syms =
- uncurry enclose (isabelle_body_delim name)
- ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
- output_known_symbols known syms);
+fun isabelle_body name =
+ enclose_body
+ ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
+ "%\n\\end{isabellebody}%\n";
fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
--- a/src/Pure/Thy/present.ML Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Pure/Thy/present.ML Fri Dec 22 21:01:53 2017 +0000
@@ -14,7 +14,6 @@
val finish: unit -> unit
val theory_output: Position.T -> theory -> Latex.text list -> unit
val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
- val display_drafts: Path.T list -> int
end;
structure Present: PRESENT =
@@ -320,51 +319,4 @@
else ();
in Browser_Info.put {chapter = chapter, name = session_name} thy end);
-
-
-(** draft document output **)
-
-fun display_drafts src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir =>
- let
- fun prep_draft path i =
- let
- val base = Path.base path;
- val name =
- (case Path.implode (#1 (Path.split_ext base)) of
- "" => "DUMMY"
- | s => s) ^ serial_string ();
- in
- if File.exists path then
- (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
- else error ("Bad file: " ^ Path.print path)
- end;
- val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0));
-
- val doc_path = Path.append dir document_path;
- val _ = Isabelle_System.mkdirs doc_path;
- val root_path = Path.append doc_path (Path.basic "root.tex");
- val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
- val _ = Isabelle_System.bash ("isabelle latex -o sty " ^ File.bash_path root_path);
- val _ = Isabelle_System.bash ("isabelle latex -o syms " ^ File.bash_path root_path);
-
- fun known name =
- let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
- in member (op =) ss end;
- val known_syms = known "syms.lst";
- val known_ctrls = known "ctrls.lst";
-
- val _ = srcs |> List.app (fn (name, base, txt) =>
- Symbol.explode txt
- |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
- |> File.write (Path.append doc_path (tex_path name)));
- val _ = write_tex_index tex_index doc_path;
-
- val result = isabelle_document {verbose = false} "pdf" documentN "" doc_path;
-
- val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp";
- val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
- val _ = Isabelle_System.mkdirs target_dir;
- val _ = Isabelle_System.copy_file result target;
- in Isabelle_System.bash ("isabelle display " ^ File.bash_path target ^ " &") end);
-
end;
--- a/src/Pure/Thy/present.scala Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Pure/Thy/present.scala Fri Dec 22 21:01:53 2017 +0000
@@ -101,7 +101,49 @@
}
- /* theory document */
+ /** preview **/
+
+ sealed case class Preview(title: String, content: String)
+
+ def preview(snapshot: Document.Snapshot,
+ plain_text: Boolean = false,
+ fonts_url: String => String = HTML.fonts_url()): Preview =
+ {
+ require(!snapshot.is_outdated)
+
+ def output_document(title: String, body: XML.Body): String =
+ HTML.output_document(
+ List(
+ HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)),
+ HTML.title(title)),
+ List(HTML.source(body)), css = "")
+
+ val name = snapshot.node_name
+ if (plain_text) {
+ val title = "File " + quote(name.path.base_name)
+ val content = output_document(title, HTML.text(snapshot.node.source))
+ Preview(title, content)
+ }
+ else if (name.is_bibtex) {
+ val title = "Bibliography " + quote(name.path.base_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)
+ }
+ Preview(title, content)
+ }
+ else {
+ val title =
+ if (name.is_theory) "Theory " + quote(name.theory_base_name)
+ else "File " + quote(name.path.base_name)
+ val content = output_document(title, pide_document(snapshot))
+ Preview(title, content)
+ }
+ }
+
+
+ /* PIDE document */
private val document_span_elements =
Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT
@@ -127,19 +169,10 @@
XML.Text(Symbol.decode(text))
}
- def theory_document(snapshot: Document.Snapshot): XML.Body =
+ def pide_document(snapshot: Document.Snapshot): XML.Body =
make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
- /* text document */
-
- def text_document(snapshot: Document.Snapshot): XML.Body =
- snapshot.node.get_text match {
- case "" => Nil
- case txt => List(XML.Text(Symbol.decode(txt)))
- }
-
-
/** build document **/
--- a/src/Pure/Tools/bibtex.scala Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Pure/Tools/bibtex.scala Fri Dec 22 21:01:53 2017 +0000
@@ -494,7 +494,7 @@
private val output_styles =
List(
- "empty" -> "html-n",
+ "" -> "html-n",
"plain" -> "html-n",
"alpha" -> "html-a",
"named" -> "html-n",
@@ -503,9 +503,10 @@
"unsortlist" -> "html-u")
def html_output(bib: List[Path],
+ title: String = "Bibliography",
body: Boolean = false,
citations: List[String] = List("*"),
- style: String = "empty",
+ style: String = "",
chronological: Boolean = false): String =
{
Isabelle_System.with_tmp_dir("bibtex")(tmp_dir =>
@@ -548,8 +549,10 @@
Isabelle_System.bash(
"\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
- " -u -s " + Bash.string(style) + (if (chronological) " -c " else " ") +
- File.bash_path(in_file) + " " + File.bash_path(out_file),
+ " -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)
@@ -563,12 +566,4 @@
else html
})
}
-
- def present(snapshot: Document.Snapshot): String =
- {
- Isabelle_System.with_tmp_file("bib", "bib") { bib =>
- File.write(bib, snapshot.node.get_text)
- html_output(List(bib), style = "unsort")
- }
- }
}
--- a/src/Tools/VSCode/extension/package.json Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Tools/VSCode/extension/package.json Fri Dec 22 21:01:53 2017 +0000
@@ -25,6 +25,7 @@
"activationEvents": [
"onLanguage:isabelle",
"onLanguage:isabelle-ml",
+ "onLanguage:bibtex",
"onCommand:isabelle.preview",
"onCommand:isabelle.preview-split",
"onCommand:isabelle.preview-source"
@@ -107,11 +108,31 @@
"group": "navigation"
},
{
+ "when": "editorLangId == isabelle-ml",
+ "command": "isabelle.preview",
+ "group": "navigation"
+ },
+ {
+ "when": "editorLangId == bibtex",
+ "command": "isabelle.preview",
+ "group": "navigation"
+ },
+ {
"when": "editorLangId == isabelle",
"command": "isabelle.preview-split",
"group": "navigation"
},
{
+ "when": "editorLangId == isabelle-ml",
+ "command": "isabelle.preview-split",
+ "group": "navigation"
+ },
+ {
+ "when": "editorLangId == bibtex",
+ "command": "isabelle.preview-split",
+ "group": "navigation"
+ },
+ {
"when": "resourceScheme == isabelle-preview",
"command": "isabelle.preview-update",
"group": "navigation"
@@ -127,6 +148,16 @@
"when": "resourceLangId == isabelle",
"command": "isabelle.preview",
"group": "navigation"
+ },
+ {
+ "when": "resourceLangId == isabelle-ml",
+ "command": "isabelle.preview",
+ "group": "navigation"
+ },
+ {
+ "when": "resourceLangId == bibtex",
+ "command": "isabelle.preview",
+ "group": "navigation"
}
]
},
@@ -492,11 +523,11 @@
"postinstall": "node ./node_modules/vscode/bin/install"
},
"devDependencies": {
- "@types/mocha": "^2.2.43",
- "@types/node": "^7.0.43",
+ "@types/mocha": "^2.2.44",
+ "@types/node": "^7.0.51",
"mocha": "^3.5.3",
- "typescript": "^2.5.2",
- "vscode": "^1.1.5"
+ "typescript": "^2.6.2",
+ "vscode": "^1.1.10"
},
"dependencies": {
"vscode-languageclient": "~3.2.2"
--- a/src/Tools/VSCode/src/document_model.scala Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Tools/VSCode/src/document_model.scala Fri Dec 22 21:01:53 2017 +0000
@@ -143,7 +143,7 @@
def get_blob: Option[Document.Blob] =
if (is_theory) None
- else Some((Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty)))
+ else Some((Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)))
/* bibtex entries */
--- a/src/Tools/VSCode/src/preview_panel.scala Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Tools/VSCode/src/preview_panel.scala Fri Dec 22 21:01:53 2017 +0000
@@ -30,8 +30,9 @@
val snapshot = model.snapshot()
if (snapshot.is_outdated) m
else {
- val (label, content) = make_preview(model, snapshot)
- channel.write(Protocol.Preview_Response(file, column, label, content))
+ val preview = Present.preview(snapshot)
+ channel.write(
+ Protocol.Preview_Response(file, column, preview.title, preview.content))
m - file
}
case None => m - file
@@ -40,15 +41,4 @@
(map1.nonEmpty, map1)
})
}
-
- def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
- {
- val label = "Preview " + quote(model.node_name.theory_base_name)
- val content =
- HTML.output_document(
- List(HTML.style(HTML.fonts_css()), HTML.style_file(HTML.isabelle_css)),
- List(HTML.source(Present.theory_document(snapshot))),
- css = "")
- (label, content)
- }
}
--- a/src/Tools/jEdit/src/actions.xml Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Tools/jEdit/src/actions.xml Fri Dec 22 21:01:53 2017 +0000
@@ -159,7 +159,12 @@
</ACTION>
<ACTION NAME="isabelle.preview">
<CODE>
- isabelle.jedit.Document_Model.open_preview(view);
+ isabelle.jedit.Document_Model.open_preview(view, false);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.draft">
+ <CODE>
+ isabelle.jedit.Document_Model.open_preview(view, true);
</CODE>
</ACTION>
<ACTION NAME="isabelle.keymap-merge">
--- a/src/Tools/jEdit/src/document_model.scala Fri Dec 22 21:00:07 2017 +0000
+++ b/src/Tools/jEdit/src/document_model.scala Fri Dec 22 21:01:53 2017 +0000
@@ -286,14 +286,16 @@
/* HTTP preview */
- def open_preview(view: View)
+ private val plain_text_prefix = "plain_text="
+
+ def open_preview(view: View, plain_text: Boolean)
{
Document_Model.get(view.getBuffer) match {
case Some(model) =>
val name = model.node_name
val url =
PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview?" +
- Url.encode(if (name.is_theory) name.theory else name.node)
+ (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
PIDE.editor.hyperlink_url(url).follow(view)
case _ =>
}
@@ -307,13 +309,17 @@
val preview =
HTTP.get(preview_root, arg =>
for {
- url_name <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_))
- model <-
- get_models().iterator.collectFirst(
- { case (name, model)
- if url_name == (if (name.is_theory) name.theory else name.node) => model })
+ query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_))
+ name = Library.perhaps_unprefix(plain_text_prefix, query)
+ model <- get(PIDE.resources.node_name(name))
}
- yield HTTP.Response.html(model.preview(fonts_root)))
+ yield {
+ val snapshot = model.await_stable_snapshot()
+ val preview =
+ Present.preview(snapshot, fonts_url = HTML.fonts_dir(fonts_root),
+ plain_text = query.startsWith(plain_text_prefix))
+ HTTP.Response.html(preview.content)
+ })
List(HTTP.fonts(fonts_root), preview)
}
@@ -321,30 +327,6 @@
sealed abstract class Document_Model extends Document.Model
{
- /* content */
-
- def bibtex_entries: List[Text.Info[String]]
-
- def preview(fonts_dir: String): String =
- {
- val snapshot = await_stable_snapshot()
-
- if (is_bibtex) Bibtex.present(snapshot)
- else {
- HTML.output_document(
- List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css))),
- css = "",
- body =
- if (is_theory)
- List(HTML.chapter("Theory " + quote(node_name.theory_base_name)),
- HTML.source(Present.theory_document(snapshot)))
- else
- List(HTML.chapter("File " + quote(node_name.node)),
- HTML.source(Present.text_document(snapshot))))
- }
- }
-
-
/* perspective */
def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
@@ -437,7 +419,7 @@
def get_blob: Option[Document.Blob] =
if (is_theory) None
- else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
+ else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
def bibtex_entries: List[Text.Info[String]] =
if (is_bibtex) content.bibtex_entries else Nil
@@ -529,7 +511,7 @@
/* blob */
// owned by GUI thread
- private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None
+ private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
@@ -537,17 +519,19 @@
GUI_Thread.require {
if (is_theory) None
else {
- val (bytes, chunk) =
+ val (bytes, text, chunk) =
_blob match {
case Some(x) => x
case None =>
val bytes = PIDE.resources.make_file_content(buffer)
- val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
- _blob = Some((bytes, chunk))
- (bytes, chunk)
+ val text = buffer.getText(0, buffer.getLength)
+ val chunk = Symbol.Text_Chunk(text)
+ val x = (bytes, text, chunk)
+ _blob = Some(x)
+ x
}
val changed = pending_edits.nonEmpty
- Some(Document.Blob(bytes, chunk, changed))
+ Some(Document.Blob(bytes, text, chunk, changed))
}
}