discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
authorwenzelm
Wed Sep 12 12:09:40 2012 +0200 (2012-09-12)
changeset 4932094bd2fb83d11
parent 49319 f4b91a3a5f0f
child 49321 a48f9bbbe720
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
lib/texinputs/isabelle.sty
src/Doc/pdfsetup.sty
src/Pure/Thy/latex.ML
     1.1 --- a/lib/texinputs/isabelle.sty	Wed Sep 12 11:38:23 2012 +0200
     1.2 +++ b/lib/texinputs/isabelle.sty	Wed Sep 12 12:09:40 2012 +0200
     1.3 @@ -103,9 +103,6 @@
     1.4  \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
     1.5  }
     1.6  
     1.7 -\newcommand{\isaliteral}[2]{#2}
     1.8 -\newcommand{\isanil}{}
     1.9 -
    1.10  
    1.11  % keyword and section markup
    1.12  
    1.13 @@ -158,9 +155,9 @@
    1.14  \isachardefaults%
    1.15  \def\isacharunderscorekeyword{\mbox{-}}%
    1.16  \def\isacharbang{\isamath{!}}%
    1.17 -\def\isachardoublequote{\isanil}%
    1.18 -\def\isachardoublequoteopen{\isanil}%
    1.19 -\def\isachardoublequoteclose{\isanil}%
    1.20 +\def\isachardoublequote{}%
    1.21 +\def\isachardoublequoteopen{}%
    1.22 +\def\isachardoublequoteclose{}%
    1.23  \def\isacharhash{\isamath{\#}}%
    1.24  \def\isachardollar{\isamath{\$}}%
    1.25  \def\isacharpercent{\isamath{\%}}%
     2.1 --- a/src/Doc/pdfsetup.sty	Wed Sep 12 11:38:23 2012 +0200
     2.2 +++ b/src/Doc/pdfsetup.sty	Wed Sep 12 12:09:40 2012 +0200
     2.3 @@ -15,13 +15,3 @@
     2.4  \urlstyle{rm}
     2.5  \ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
     2.6  
     2.7 -\def\isaliteral#1#2{#2}
     2.8 -\def\isanil{}
     2.9 -
    2.10 -%experimental treatment of replacement text
    2.11 -\iffalse
    2.12 -\ifnum\pdfminorversion<5\pdfminorversion=5\fi
    2.13 -\renewcommand{\isaliteral}[2]{%
    2.14 -\pdfliteral direct{/Span <</ActualText<#1>>> BDC}#2\pdfliteral direct{EMC}}
    2.15 -\renewcommand{\isanil}{{\color{white}.}}
    2.16 -\fi
     3.1 --- a/src/Pure/Thy/latex.ML	Wed Sep 12 11:38:23 2012 +0200
     3.2 +++ b/src/Pure/Thy/latex.ML	Wed Sep 12 12:09:40 2012 +0200
     3.3 @@ -30,22 +30,6 @@
     3.4  structure Latex: LATEX =
     3.5  struct
     3.6  
     3.7 -(* literal text *)
     3.8 -
     3.9 -local
    3.10 -  fun hex_nibble i =
    3.11 -    if i < 10 then string_of_int i
    3.12 -    else chr (ord "A" + i - 10);
    3.13 -
    3.14 -  fun hex_byte c = hex_nibble (ord c div 16) ^ hex_nibble (ord c mod 16);
    3.15 -in
    3.16 -
    3.17 -fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}";
    3.18 -fun enclose_literal txt arg = enclose "{" "}" (literal txt ^ arg);
    3.19 -
    3.20 -end;
    3.21 -
    3.22 -
    3.23  (* symbol output *)
    3.24  
    3.25  local
    3.26 @@ -90,7 +74,7 @@
    3.27    | output_chr "\n" = "\\isanewline\n"
    3.28    | output_chr c =
    3.29        (case Symtab.lookup char_table c of
    3.30 -        SOME s => enclose_literal c s
    3.31 +        SOME s => s
    3.32        | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
    3.33  
    3.34  val output_chrs = translate_string output_chr;
    3.35 @@ -99,12 +83,8 @@
    3.36    (case Symbol.decode sym of
    3.37      Symbol.Char s => output_chr s
    3.38    | Symbol.UTF8 s => s
    3.39 -  | Symbol.Sym s =>
    3.40 -      if known_sym s then enclose_literal sym (enclose "{\\isasym" "}" s)
    3.41 -      else output_chrs sym
    3.42 -  | Symbol.Ctrl s =>
    3.43 -      if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s
    3.44 -      else output_chrs sym
    3.45 +  | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
    3.46 +  | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
    3.47    | Symbol.Raw s => s
    3.48    | Symbol.Malformed s => error (Symbol.malformed_msg s)
    3.49    | Symbol.EOF => error "Bad EOF symbol");
    3.50 @@ -120,8 +100,8 @@
    3.51      | Antiquote.Antiq (ss, _) =>
    3.52          enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
    3.53            (output_symbols (map Symbol_Pos.symbol ss))
    3.54 -    | Antiquote.Open _ => enclose_literal "\\<lbrace>" "{\\isaantiqopen}"
    3.55 -    | Antiquote.Close _ => enclose_literal "\\<rbrace>" "{\\isaantiqclose}");
    3.56 +    | Antiquote.Open _ => "{\\isaantiqopen}"
    3.57 +    | Antiquote.Close _ => "{\\isaantiqclose}");
    3.58  
    3.59  end;
    3.60  
    3.61 @@ -138,23 +118,15 @@
    3.62      else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then
    3.63        "\\isakeyword{" ^ output_syms s ^ "}"
    3.64      else if Token.is_kind Token.String tok then
    3.65 -      output_syms s |> enclose
    3.66 -        (enclose_literal "\"" "{\\isachardoublequoteopen}")
    3.67 -        (enclose_literal "\"" "{\\isachardoublequoteclose}")
    3.68 +      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
    3.69      else if Token.is_kind Token.AltString tok then
    3.70 -      output_syms s |> enclose
    3.71 -        (enclose_literal "`" "{\\isacharbackquoteopen}")
    3.72 -        (enclose_literal "`" "{\\isacharbackquoteclose}")
    3.73 +      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
    3.74      else if Token.is_kind Token.Verbatim tok then
    3.75        let
    3.76          val (txt, pos) = Token.source_position_of tok;
    3.77          val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
    3.78          val out = implode (map output_syms_antiq ants);
    3.79 -      in
    3.80 -        out |> enclose
    3.81 -          (enclose_literal "{*" "{\\isacharverbatimopen}")
    3.82 -          (enclose_literal "*}" "{\\isacharverbatimclose}")
    3.83 -      end
    3.84 +      in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    3.85      else output_syms s
    3.86    end;
    3.87