discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);

--- a/lib/texinputs/isabelle.sty	Wed Sep 12 11:38:23 2012 +0200
+++ b/lib/texinputs/isabelle.sty	Wed Sep 12 12:09:40 2012 +0200
@@ -103,9 +103,6 @@
 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
 }
 
-\newcommand{\isaliteral}[2]{#2}
-\newcommand{\isanil}{}
-
 
 % keyword and section markup
 
@@ -158,9 +155,9 @@
 \isachardefaults%
 \def\isacharunderscorekeyword{\mbox{-}}%
 \def\isacharbang{\isamath{!}}%
-\def\isachardoublequote{\isanil}%
-\def\isachardoublequoteopen{\isanil}%
-\def\isachardoublequoteclose{\isanil}%
+\def\isachardoublequote{}%
+\def\isachardoublequoteopen{}%
+\def\isachardoublequoteclose{}%
 \def\isacharhash{\isamath{\#}}%
 \def\isachardollar{\isamath{\$}}%
 \def\isacharpercent{\isamath{\%}}%

--- a/src/Doc/pdfsetup.sty	Wed Sep 12 11:38:23 2012 +0200
+++ b/src/Doc/pdfsetup.sty	Wed Sep 12 12:09:40 2012 +0200
@@ -15,13 +15,3 @@
 \urlstyle{rm}
 \ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
 
-\def\isaliteral#1#2{#2}
-\def\isanil{}
-
-%experimental treatment of replacement text
-\iffalse
-\ifnum\pdfminorversion<5\pdfminorversion=5\fi
-\renewcommand{\isaliteral}[2]{%
-\pdfliteral direct{/Span <</ActualText<#1>>> BDC}#2\pdfliteral direct{EMC}}
-\renewcommand{\isanil}{{\color{white}.}}
-\fi

--- a/src/Pure/Thy/latex.ML	Wed Sep 12 11:38:23 2012 +0200
+++ b/src/Pure/Thy/latex.ML	Wed Sep 12 12:09:40 2012 +0200
@@ -30,22 +30,6 @@
 structure Latex: LATEX =
 struct
 
-(* literal text *)
-
-local
-  fun hex_nibble i =
-    if i < 10 then string_of_int i
-    else chr (ord "A" + i - 10);
-
-  fun hex_byte c = hex_nibble (ord c div 16) ^ hex_nibble (ord c mod 16);
-in
-
-fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}";
-fun enclose_literal txt arg = enclose "{" "}" (literal txt ^ arg);
-
-end;
-
-
 (* symbol output *)
 
 local
@@ -90,7 +74,7 @@
   | output_chr "\n" = "\\isanewline\n"
   | output_chr c =
       (case Symtab.lookup char_table c of
-        SOME s => enclose_literal c s
+        SOME s => s
       | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
 
 val output_chrs = translate_string output_chr;
@@ -99,12 +83,8 @@
   (case Symbol.decode sym of
     Symbol.Char s => output_chr s
   | Symbol.UTF8 s => s
-  | Symbol.Sym s =>
-      if known_sym s then enclose_literal sym (enclose "{\\isasym" "}" s)
-      else output_chrs sym
-  | Symbol.Ctrl s =>
-      if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s
-      else output_chrs sym
+  | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
+  | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
   | Symbol.Raw s => s
   | Symbol.Malformed s => error (Symbol.malformed_msg s)
   | Symbol.EOF => error "Bad EOF symbol");
@@ -120,8 +100,8 @@
     | Antiquote.Antiq (ss, _) =>
         enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
           (output_symbols (map Symbol_Pos.symbol ss))
-    | Antiquote.Open _ => enclose_literal "\\<lbrace>" "{\\isaantiqopen}"
-    | Antiquote.Close _ => enclose_literal "\\<rbrace>" "{\\isaantiqclose}");
+    | Antiquote.Open _ => "{\\isaantiqopen}"
+    | Antiquote.Close _ => "{\\isaantiqclose}");
 
 end;
 
@@ -138,23 +118,15 @@
     else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then
       "\\isakeyword{" ^ output_syms s ^ "}"
     else if Token.is_kind Token.String tok then
-      output_syms s |> enclose
-        (enclose_literal "\"" "{\\isachardoublequoteopen}")
-        (enclose_literal "\"" "{\\isachardoublequoteclose}")
+      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
     else if Token.is_kind Token.AltString tok then
-      output_syms s |> enclose
-        (enclose_literal "`" "{\\isacharbackquoteopen}")
-        (enclose_literal "`" "{\\isacharbackquoteclose}")
+      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
     else if Token.is_kind Token.Verbatim tok then
       let
         val (txt, pos) = Token.source_position_of tok;
         val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
         val out = implode (map output_syms_antiq ants);
-      in
-        out |> enclose
-          (enclose_literal "{*" "{\\isacharverbatimopen}")
-          (enclose_literal "*}" "{\\isacharverbatimclose}")
-      end
+      in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
     else output_syms s
   end;