# HG changeset patch
# User wenzelm
# Date 1289166676 -3600
# Node ID b646316f8b3c7decebb130e85b61ce9b590dd01a
# Parent  25ba6b2559e11c52c684555996fc8342308b47d5
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;

diff -r 25ba6b2559e1 -r b646316f8b3c doc-src/isabelle.sty
--- a/doc-src/isabelle.sty	Sun Nov 07 22:42:49 2010 +0100
+++ b/doc-src/isabelle.sty	Sun Nov 07 22:51:16 2010 +0100
@@ -95,6 +95,8 @@
 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
 }
 
+\newcommand{\isaliteral}[2]{#2}
+
 
 % keyword and section markup
 
diff -r 25ba6b2559e1 -r b646316f8b3c doc-src/pdfsetup.sty
--- a/doc-src/pdfsetup.sty	Sun Nov 07 22:42:49 2010 +0100
+++ b/doc-src/pdfsetup.sty	Sun Nov 07 22:51:16 2010 +0100
@@ -15,3 +15,9 @@
 \urlstyle{rm}
 
 \ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
+
+\ifpdf
+\ifnum\pdfminorversion<5\pdfminorversion=5\fi
+\renewcommand{\isaliteral}[2]{%
+\pdfliteral direct{/Span <</ActualText<#1>>> BDC}#2\pdfliteral direct{EMC}}
+\fi
diff -r 25ba6b2559e1 -r b646316f8b3c lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Sun Nov 07 22:42:49 2010 +0100
+++ b/lib/texinputs/isabelle.sty	Sun Nov 07 22:51:16 2010 +0100
@@ -95,6 +95,8 @@
 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
 }
 
+\newcommand{\isaliteral}[2]{#2}
+
 
 % keyword and section markup
 
diff -r 25ba6b2559e1 -r b646316f8b3c src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Nov 07 22:42:49 2010 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Nov 07 22:51:16 2010 +0100
@@ -30,47 +30,64 @@
 structure Latex: LATEX =
 struct
 
+(* literal text *)
+
+local
+  val hex = Int.fmt StringCvt.HEX;
+  fun hex_byte c = hex (ord c div 16) ^ hex (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
 
-val output_chr = fn
-  " " => "\\ " |
-  "\n" => "\\isanewline\n" |
-  "!" => "{\\isacharbang}" |
-  "\"" => "{\\isachardoublequote}" |
-  "#" => "{\\isacharhash}" |
-  "$" => "{\\isachardollar}" |
-  "%" => "{\\isacharpercent}" |
-  "&" => "{\\isacharampersand}" |
-  "'" => "{\\isacharprime}" |
-  "(" => "{\\isacharparenleft}" |
-  ")" => "{\\isacharparenright}" |
-  "*" => "{\\isacharasterisk}" |
-  "+" => "{\\isacharplus}" |
-  "," => "{\\isacharcomma}" |
-  "-" => "{\\isacharminus}" |
-  "." => "{\\isachardot}" |
-  "/" => "{\\isacharslash}" |
-  ":" => "{\\isacharcolon}" |
-  ";" => "{\\isacharsemicolon}" |
-  "<" => "{\\isacharless}" |
-  "=" => "{\\isacharequal}" |
-  ">" => "{\\isachargreater}" |
-  "?" => "{\\isacharquery}" |
-  "@" => "{\\isacharat}" |
-  "[" => "{\\isacharbrackleft}" |
-  "\\" => "{\\isacharbackslash}" |
-  "]" => "{\\isacharbrackright}" |
-  "^" => "{\\isacharcircum}" |
-  "_" => "{\\isacharunderscore}" |
-  "`" => "{\\isacharbackquote}" |
-  "{" => "{\\isacharbraceleft}" |
-  "|" => "{\\isacharbar}" |
-  "}" => "{\\isacharbraceright}" |
-  "~" => "{\\isachartilde}" |
-  c => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c;
+val char_table =
+  Symtab.make
+   [("!", "{\\isacharbang}"),
+    ("\"", "{\\isachardoublequote}"),
+    ("#", "{\\isacharhash}"),
+    ("$", "{\\isachardollar}"),
+    ("%", "{\\isacharpercent}"),
+    ("&", "{\\isacharampersand}"),
+    ("'", "{\\isacharprime}"),
+    ("(", "{\\isacharparenleft}"),
+    (")", "{\\isacharparenright}"),
+    ("*", "{\\isacharasterisk}"),
+    ("+", "{\\isacharplus}"),
+    (",", "{\\isacharcomma}"),
+    ("-", "{\\isacharminus}"),
+    (".", "{\\isachardot}"),
+    ("/", "{\\isacharslash}"),
+    (":", "{\\isacharcolon}"),
+    (";", "{\\isacharsemicolon}"),
+    ("<", "{\\isacharless}"),
+    ("=", "{\\isacharequal}"),
+    (">", "{\\isachargreater}"),
+    ("?", "{\\isacharquery}"),
+    ("@", "{\\isacharat}"),
+    ("[", "{\\isacharbrackleft}"),
+    ("\\", "{\\isacharbackslash}"),
+    ("]", "{\\isacharbrackright}"),
+    ("^", "{\\isacharcircum}"),
+    ("_", "{\\isacharunderscore}"),
+    ("`", "{\\isacharbackquote}"),
+    ("{", "{\\isacharbraceleft}"),
+    ("|", "{\\isacharbar}"),
+    ("}", "{\\isacharbraceright}"),
+    ("~", "{\\isachartilde}")];
+
+fun output_chr " " = "\\ "
+  | output_chr "\n" = "\\isanewline\n"
+  | output_chr c =
+      (case Symtab.lookup char_table c of
+        SOME s => enclose_literal c s
+      | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
 
 val output_chrs = translate_string output_chr;
 
@@ -78,8 +95,12 @@
   (case Symbol.decode sym of
     Symbol.Char s => output_chr s
   | Symbol.UTF8 s => s
-  | 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.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.Raw s => s);
 
 in
@@ -91,9 +112,10 @@
 val output_syms_antiq =
   (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
     | Antiquote.Antiq (ss, _) =>
-        enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
-    | Antiquote.Open _ => "{\\isaantiqopen}"
-    | Antiquote.Close _ => "{\\isaantiqclose}");
+        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}");
 
 end;
 
@@ -110,15 +132,23 @@
     else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then
       "\\isakeyword{" ^ output_syms s ^ "}"
     else if Token.is_kind Token.String tok then
-      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
+      output_syms s |> enclose
+        (enclose_literal "\"" "{\\isachardoublequoteopen}")
+        (enclose_literal "\"" "{\\isachardoublequoteclose}")
     else if Token.is_kind Token.AltString tok then
-      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
+      output_syms s |> enclose
+        (enclose_literal "`" "{\\isacharbackquoteopen}")
+        (enclose_literal "`" "{\\isacharbackquoteclose}")
     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 enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
+      in
+        out |> enclose
+          (enclose_literal "{*" "{\\isacharverbatimopen}")
+          (enclose_literal "*}" "{\\isacharverbatimclose}")
+      end
     else output_syms s
   end;