--- a/Admin/Release/CHECKLIST Fri Dec 22 17:49:51 2017 +0100
+++ b/Admin/Release/CHECKLIST Fri Dec 22 18:32:59 2017 +0100
@@ -5,8 +5,6 @@
- check Admin/components;
-- test 'display_drafts' command;
-
- test Isabelle/jEdit: print buffer
- test "#!/usr/bin/env isabelle_scala_script";
--- a/NEWS Fri Dec 22 17:49:51 2017 +0100
+++ b/NEWS Fri Dec 22 18:32:59 2017 +0100
@@ -41,6 +41,9 @@
isabelle build -D '~~/src/ZF'
+* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
+use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
+
*** Isabelle/jEdit Prover IDE ***
--- a/lib/Tools/latex Fri Dec 22 17:49:51 2017 +0100
+++ b/lib/Tools/latex Fri Dec 22 18:32:59 2017 +0100
@@ -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/texinputs/draft.tex Fri Dec 22 17:49:51 2017 +0100
+++ /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 17:49:51 2017 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Dec 22 18:32:59 2017 +0100
@@ -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/System/Presentation.thy Fri Dec 22 17:49:51 2017 +0100
+++ b/src/Doc/System/Presentation.thy Fri Dec 22 18:32:59 2017 +0100
@@ -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/Pure.thy Fri Dec 22 17:49:51 2017 +0100
+++ b/src/Pure/Pure.thy Fri Dec 22 18:32:59 2017 +0100
@@ -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/latex.ML Fri Dec 22 17:49:51 2017 +0100
+++ b/src/Pure/Thy/latex.ML Fri Dec 22 18:32:59 2017 +0100
@@ -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 17:49:51 2017 +0100
+++ b/src/Pure/Thy/present.ML Fri Dec 22 18:32:59 2017 +0100
@@ -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;