discontinued 'display_drafts' command;
authorwenzelm
Fri Dec 22 18:32:59 2017 +0100 (2017-12-22)
changeset 67263449a989f42cd
parent 67262 46540a2ead4b
child 67264 16f74b7c248a
discontinued 'display_drafts' command;
Admin/Release/CHECKLIST
NEWS
lib/Tools/latex
lib/texinputs/draft.tex
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/System/Presentation.thy
src/Pure/Pure.thy
src/Pure/Thy/latex.ML
src/Pure/Thy/present.ML
     1.1 --- a/Admin/Release/CHECKLIST	Fri Dec 22 17:49:51 2017 +0100
     1.2 +++ b/Admin/Release/CHECKLIST	Fri Dec 22 18:32:59 2017 +0100
     1.3 @@ -5,8 +5,6 @@
     1.4  
     1.5  - check Admin/components;
     1.6  
     1.7 -- test 'display_drafts' command;
     1.8 -
     1.9  - test Isabelle/jEdit: print buffer
    1.10  
    1.11  - test "#!/usr/bin/env isabelle_scala_script";
     2.1 --- a/NEWS	Fri Dec 22 17:49:51 2017 +0100
     2.2 +++ b/NEWS	Fri Dec 22 18:32:59 2017 +0100
     2.3 @@ -41,6 +41,9 @@
     2.4  
     2.5    isabelle build -D '~~/src/ZF'
     2.6  
     2.7 +* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
     2.8 +use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
     2.9 +
    2.10  
    2.11  *** Isabelle/jEdit Prover IDE ***
    2.12  
     3.1 --- a/lib/Tools/latex	Fri Dec 22 17:49:51 2017 +0100
     3.2 +++ b/lib/Tools/latex	Fri Dec 22 18:32:59 2017 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4    echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
     3.5    echo
     3.6    echo "  Options are:"
     3.7 -  echo "    -o FORMAT    specify output format: pdf (default), dvi, bbl, idx, sty, syms"
     3.8 +  echo "    -o FORMAT    specify output format: pdf (default), dvi, bbl, idx, sty"
     3.9    echo
    3.10    echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    3.11    echo "  producing the specified output format."
    3.12 @@ -83,16 +83,6 @@
    3.13    done
    3.14  }
    3.15  
    3.16 -function extract_syms ()
    3.17 -{
    3.18 -  perl -n \
    3.19 -    -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
    3.20 -    "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
    3.21 -  perl -n \
    3.22 -    -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
    3.23 -    "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
    3.24 -}
    3.25 -
    3.26  case "$OUTFORMAT" in
    3.27    pdf)
    3.28      check_root && \
    3.29 @@ -118,10 +108,6 @@
    3.30      copy_styles
    3.31      RC="$?"
    3.32      ;;
    3.33 -  syms)
    3.34 -    extract_syms
    3.35 -    RC="$?"
    3.36 -    ;;
    3.37    *)
    3.38      fail "Bad output format '$OUTFORMAT'"
    3.39      ;;
     4.1 --- a/lib/texinputs/draft.tex	Fri Dec 22 17:49:51 2017 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,24 +0,0 @@
     4.4 -%%
     4.5 -%% root for draft documents
     4.6 -%%
     4.7 -
     4.8 -\documentclass[10pt,a4paper]{article}
     4.9 -\usepackage{isabelle,isabellesym,pdfsetup}
    4.10 -
    4.11 -%packages for unusual symbols according to 'isabelle latex -o syms'
    4.12 -\usepackage{amssymb}
    4.13 -\usepackage{textcomp}
    4.14 -
    4.15 -\pagestyle{myheadings}
    4.16 -\newcommand{\isamarkupfile}[1]%
    4.17 -{{\def\isacharunderscore{\mbox{-}}%
    4.18 -\section*{#1}\markright{FILE~``\isabellecontext''}}}
    4.19 -
    4.20 -\begin{document}
    4.21 -\input{session}
    4.22 -\end{document}
    4.23 -
    4.24 -%%% Local Variables:
    4.25 -%%% mode: latex
    4.26 -%%% TeX-master: t
    4.27 -%%% End:
     5.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Dec 22 17:49:51 2017 +0100
     5.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Dec 22 18:32:59 2017 +0100
     5.3 @@ -613,21 +613,4 @@
     5.4    @{rail \<open>A + sep\<close>}
     5.5  \<close>
     5.6  
     5.7 -
     5.8 -section \<open>Draft presentation\<close>
     5.9 -
    5.10 -text \<open>
    5.11 -  \begin{matharray}{rcl}
    5.12 -    @{command_def "display_drafts"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
    5.13 -  \end{matharray}
    5.14 -
    5.15 -  @{rail \<open>
    5.16 -    @@{command display_drafts} (@{syntax name} +)
    5.17 -  \<close>}
    5.18 -
    5.19 -  \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a given list
    5.20 -  of raw source files. Only those symbols that do not require additional
    5.21 -  {\LaTeX} packages are displayed properly, everything else is left verbatim.
    5.22 -\<close>
    5.23 -
    5.24  end
     6.1 --- a/src/Doc/System/Presentation.thy	Fri Dec 22 17:49:51 2017 +0100
     6.2 +++ b/src/Doc/System/Presentation.thy	Fri Dec 22 18:32:59 2017 +0100
     6.3 @@ -254,8 +254,7 @@
     6.4  \<open>Usage: isabelle latex [OPTIONS] [FILE]
     6.5  
     6.6    Options are:
     6.7 -    -o FORMAT    specify output format: pdf (default), dvi,
     6.8 -                 bbl, idx, sty, syms
     6.9 +    -o FORMAT    specify output format: pdf (default), dvi, bbl, idx, sty
    6.10  
    6.11    Run LaTeX (and related tools) on FILE (default root.tex),
    6.12    producing the specified output format.\<close>}
    6.13 @@ -269,9 +268,6 @@
    6.14    The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
    6.15    the distribution. This is useful in special situations where the document
    6.16    sources are to be processed another time by separate tools.
    6.17 -
    6.18 -  The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists of symbols that
    6.19 -  are available without loading additional {\LaTeX} packages.
    6.20  \<close>
    6.21  
    6.22  
     7.1 --- a/src/Pure/Pure.thy	Fri Dec 22 17:49:51 2017 +0100
     7.2 +++ b/src/Pure/Pure.thy	Fri Dec 22 18:32:59 2017 +0100
     7.3 @@ -84,7 +84,7 @@
     7.4      "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
     7.5      "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
     7.6      "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
     7.7 -  and "display_drafts" "print_state" :: diag
     7.8 +  and "print_state" :: diag
     7.9    and "welcome" :: diag
    7.10    and "end" :: thy_end % "theory"
    7.11    and "realizers" :: thy_decl
    7.12 @@ -1208,12 +1208,6 @@
    7.13    Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"
    7.14      (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
    7.15  
    7.16 -val _ =
    7.17 -  Outer_Syntax.command \<^command_keyword>\<open>display_drafts\<close>
    7.18 -    "display raw source files with symbols"
    7.19 -    (Scan.repeat1 Parse.path >> (fn names =>
    7.20 -      Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
    7.21 -
    7.22  in end\<close>
    7.23  
    7.24  
     8.1 --- a/src/Pure/Thy/latex.ML	Fri Dec 22 17:49:51 2017 +0100
     8.2 +++ b/src/Pure/Thy/latex.ML	Fri Dec 22 18:32:59 2017 +0100
     8.3 @@ -18,8 +18,6 @@
     8.4    val latex_control: Symbol.symbol
     8.5    val is_latex_control: Symbol.symbol -> bool
     8.6    val embed_raw: string -> string
     8.7 -  val output_known_symbols: (string -> bool) * (string -> bool) ->
     8.8 -    Symbol.symbol list -> string
     8.9    val output_symbols: Symbol.symbol list -> string
    8.10    val output_syms: string -> string
    8.11    val output_token: Token.T -> string
    8.12 @@ -30,8 +28,6 @@
    8.13    val environment_block: string -> text list -> text
    8.14    val environment: string -> string -> string
    8.15    val isabelle_body: string -> text list -> text list
    8.16 -  val symbol_source: (string -> bool) * (string -> bool) ->
    8.17 -    string -> Symbol.symbol list -> string
    8.18    val theory_entry: string -> string
    8.19    val latexN: string
    8.20  end;
    8.21 @@ -169,14 +165,12 @@
    8.22          SOME s => s
    8.23        | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
    8.24  
    8.25 -val output_chrs = translate_string output_chr;
    8.26 -
    8.27 -fun output_known_sym (known_sym, known_ctrl) sym =
    8.28 +fun output_sym sym =
    8.29    (case Symbol.decode sym of
    8.30      Symbol.Char s => output_chr s
    8.31    | Symbol.UTF8 s => s
    8.32 -  | Symbol.Sym s => if known_sym s then enclose_name "{\\isasym" "}" s else output_chrs sym
    8.33 -  | Symbol.Control s => if known_ctrl s then enclose_name "\\isactrl" " " s else output_chrs sym
    8.34 +  | Symbol.Sym s => enclose_name "{\\isasym" "}" s
    8.35 +  | Symbol.Control s => enclose_name "\\isactrl" " " s
    8.36    | Symbol.Malformed s => error (Symbol.malformed_msg s)
    8.37    | Symbol.EOF => error "Bad EOF symbol");
    8.38  
    8.39 @@ -186,10 +180,10 @@
    8.40    Scan.one (is_latex_control o Symbol_Pos.symbol) --
    8.41      Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
    8.42  
    8.43 -fun scan_latex known =
    8.44 +val scan_latex =
    8.45    Scan.one (is_latex_control o Symbol_Pos.symbol) |--
    8.46      Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) ||
    8.47 -  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol);
    8.48 +  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol);
    8.49  
    8.50  fun read scan syms =
    8.51    Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
    8.52 @@ -199,14 +193,13 @@
    8.53  fun length_symbols syms =
    8.54    fold Integer.add (these (read scan_latex_length syms)) 0;
    8.55  
    8.56 -fun output_known_symbols known syms =
    8.57 +fun output_symbols syms =
    8.58    if exists is_latex_control syms then
    8.59 -    (case read (scan_latex known) syms of
    8.60 +    (case read scan_latex syms of
    8.61        SOME ss => implode ss
    8.62      | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
    8.63 -  else implode (map (output_known_sym known) syms);
    8.64 +  else implode (map output_sym syms);
    8.65  
    8.66 -val output_symbols = output_known_symbols (K true, K true);
    8.67  val output_syms = output_symbols o Symbol.explode;
    8.68  
    8.69  val output_syms_antiq =
    8.70 @@ -265,16 +258,10 @@
    8.71  fun environment_block name = environment_delim name |-> enclose_body #> block;
    8.72  fun environment name = environment_delim name |-> enclose;
    8.73  
    8.74 -fun isabelle_body_delim name =
    8.75 - ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n",
    8.76 -  "%\n\\end{isabellebody}%\n");
    8.77 -
    8.78 -fun isabelle_body name = isabelle_body_delim name |-> enclose_body;
    8.79 -
    8.80 -fun symbol_source known name syms =
    8.81 -  uncurry enclose (isabelle_body_delim name)
    8.82 -    ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
    8.83 -      output_known_symbols known syms);
    8.84 +fun isabelle_body name =
    8.85 +  enclose_body
    8.86 +   ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
    8.87 +   "%\n\\end{isabellebody}%\n";
    8.88  
    8.89  fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
    8.90  
     9.1 --- a/src/Pure/Thy/present.ML	Fri Dec 22 17:49:51 2017 +0100
     9.2 +++ b/src/Pure/Thy/present.ML	Fri Dec 22 18:32:59 2017 +0100
     9.3 @@ -14,7 +14,6 @@
     9.4    val finish: unit -> unit
     9.5    val theory_output: Position.T -> theory -> Latex.text list -> unit
     9.6    val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
     9.7 -  val display_drafts: Path.T list -> int
     9.8  end;
     9.9  
    9.10  structure Present: PRESENT =
    9.11 @@ -320,51 +319,4 @@
    9.12          else ();
    9.13      in Browser_Info.put {chapter = chapter, name = session_name} thy end);
    9.14  
    9.15 -
    9.16 -
    9.17 -(** draft document output **)
    9.18 -
    9.19 -fun display_drafts src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir =>
    9.20 -  let
    9.21 -    fun prep_draft path i =
    9.22 -      let
    9.23 -        val base = Path.base path;
    9.24 -        val name =
    9.25 -          (case Path.implode (#1 (Path.split_ext base)) of
    9.26 -            "" => "DUMMY"
    9.27 -          | s => s)  ^ serial_string ();
    9.28 -      in
    9.29 -        if File.exists path then
    9.30 -          (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
    9.31 -        else error ("Bad file: " ^ Path.print path)
    9.32 -      end;
    9.33 -    val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0));
    9.34 -
    9.35 -    val doc_path = Path.append dir document_path;
    9.36 -    val _ = Isabelle_System.mkdirs doc_path;
    9.37 -    val root_path = Path.append doc_path (Path.basic "root.tex");
    9.38 -    val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
    9.39 -    val _ = Isabelle_System.bash ("isabelle latex -o sty " ^ File.bash_path root_path);
    9.40 -    val _ = Isabelle_System.bash ("isabelle latex -o syms " ^ File.bash_path root_path);
    9.41 -
    9.42 -    fun known name =
    9.43 -      let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
    9.44 -      in member (op =) ss end;
    9.45 -    val known_syms = known "syms.lst";
    9.46 -    val known_ctrls = known "ctrls.lst";
    9.47 -
    9.48 -    val _ = srcs |> List.app (fn (name, base, txt) =>
    9.49 -      Symbol.explode txt
    9.50 -      |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
    9.51 -      |> File.write (Path.append doc_path (tex_path name)));
    9.52 -    val _ = write_tex_index tex_index doc_path;
    9.53 -
    9.54 -    val result = isabelle_document {verbose = false} "pdf" documentN "" doc_path;
    9.55 -
    9.56 -    val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp";
    9.57 -    val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
    9.58 -    val _ = Isabelle_System.mkdirs target_dir;
    9.59 -    val _ = Isabelle_System.copy_file result target;
    9.60 -  in Isabelle_System.bash ("isabelle display " ^ File.bash_path target ^ " &") end);
    9.61 -
    9.62  end;