# HG changeset patch
# User wenzelm
# Date 1513963979 -3600
# Node ID 449a989f42cd8327c3bcfb77ed634289c7f70af9
# Parent  46540a2ead4bc3185fff1048859166782e7e88a0
discontinued 'display_drafts' command;

diff -r 46540a2ead4b -r 449a989f42cd Admin/Release/CHECKLIST
--- 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";
diff -r 46540a2ead4b -r 449a989f42cd NEWS
--- 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 ***
 
diff -r 46540a2ead4b -r 449a989f42cd lib/Tools/latex
--- 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'"
     ;;
diff -r 46540a2ead4b -r 449a989f42cd lib/texinputs/draft.tex
--- 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:
diff -r 46540a2ead4b -r 449a989f42cd src/Doc/Isar_Ref/Document_Preparation.thy
--- 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
diff -r 46540a2ead4b -r 449a989f42cd src/Doc/System/Presentation.thy
--- 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>
 
 
diff -r 46540a2ead4b -r 449a989f42cd src/Pure/Pure.thy
--- 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>
 
 
diff -r 46540a2ead4b -r 449a989f42cd src/Pure/Thy/latex.ML
--- 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";
 
diff -r 46540a2ead4b -r 449a989f42cd src/Pure/Thy/present.ML
--- 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;