basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
authorwenzelm
Sun Nov 07 22:51:16 2010 +0100 (2010-11-07)
changeset 40402b646316f8b3c
parent 40401 25ba6b2559e1
child 40404 c1cd5437afe8
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
doc-src/isabelle.sty
doc-src/pdfsetup.sty
lib/texinputs/isabelle.sty
src/Pure/Thy/latex.ML
     1.1 --- a/doc-src/isabelle.sty	Sun Nov 07 22:42:49 2010 +0100
     1.2 +++ b/doc-src/isabelle.sty	Sun Nov 07 22:51:16 2010 +0100
     1.3 @@ -95,6 +95,8 @@
     1.4  \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
     1.5  }
     1.6  
     1.7 +\newcommand{\isaliteral}[2]{#2}
     1.8 +
     1.9  
    1.10  % keyword and section markup
    1.11  
     2.1 --- a/doc-src/pdfsetup.sty	Sun Nov 07 22:42:49 2010 +0100
     2.2 +++ b/doc-src/pdfsetup.sty	Sun Nov 07 22:51:16 2010 +0100
     2.3 @@ -15,3 +15,9 @@
     2.4  \urlstyle{rm}
     2.5  
     2.6  \ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
     2.7 +
     2.8 +\ifpdf
     2.9 +\ifnum\pdfminorversion<5\pdfminorversion=5\fi
    2.10 +\renewcommand{\isaliteral}[2]{%
    2.11 +\pdfliteral direct{/Span <</ActualText<#1>>> BDC}#2\pdfliteral direct{EMC}}
    2.12 +\fi
     3.1 --- a/lib/texinputs/isabelle.sty	Sun Nov 07 22:42:49 2010 +0100
     3.2 +++ b/lib/texinputs/isabelle.sty	Sun Nov 07 22:51:16 2010 +0100
     3.3 @@ -95,6 +95,8 @@
     3.4  \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
     3.5  }
     3.6  
     3.7 +\newcommand{\isaliteral}[2]{#2}
     3.8 +
     3.9  
    3.10  % keyword and section markup
    3.11  
     4.1 --- a/src/Pure/Thy/latex.ML	Sun Nov 07 22:42:49 2010 +0100
     4.2 +++ b/src/Pure/Thy/latex.ML	Sun Nov 07 22:51:16 2010 +0100
     4.3 @@ -30,47 +30,64 @@
     4.4  structure Latex: LATEX =
     4.5  struct
     4.6  
     4.7 +(* literal text *)
     4.8 +
     4.9 +local
    4.10 +  val hex = Int.fmt StringCvt.HEX;
    4.11 +  fun hex_byte c = hex (ord c div 16) ^ hex (ord c mod 16);
    4.12 +in
    4.13 +
    4.14 +fun literal txt = "\\isaliteral{" ^ translate_string hex_byte txt ^ "}";
    4.15 +fun enclose_literal txt arg = enclose "{" "}" (literal txt ^ arg);
    4.16 +
    4.17 +end;
    4.18 +
    4.19  
    4.20  (* symbol output *)
    4.21  
    4.22  local
    4.23  
    4.24 -val output_chr = fn
    4.25 -  " " => "\\ " |
    4.26 -  "\n" => "\\isanewline\n" |
    4.27 -  "!" => "{\\isacharbang}" |
    4.28 -  "\"" => "{\\isachardoublequote}" |
    4.29 -  "#" => "{\\isacharhash}" |
    4.30 -  "$" => "{\\isachardollar}" |
    4.31 -  "%" => "{\\isacharpercent}" |
    4.32 -  "&" => "{\\isacharampersand}" |
    4.33 -  "'" => "{\\isacharprime}" |
    4.34 -  "(" => "{\\isacharparenleft}" |
    4.35 -  ")" => "{\\isacharparenright}" |
    4.36 -  "*" => "{\\isacharasterisk}" |
    4.37 -  "+" => "{\\isacharplus}" |
    4.38 -  "," => "{\\isacharcomma}" |
    4.39 -  "-" => "{\\isacharminus}" |
    4.40 -  "." => "{\\isachardot}" |
    4.41 -  "/" => "{\\isacharslash}" |
    4.42 -  ":" => "{\\isacharcolon}" |
    4.43 -  ";" => "{\\isacharsemicolon}" |
    4.44 -  "<" => "{\\isacharless}" |
    4.45 -  "=" => "{\\isacharequal}" |
    4.46 -  ">" => "{\\isachargreater}" |
    4.47 -  "?" => "{\\isacharquery}" |
    4.48 -  "@" => "{\\isacharat}" |
    4.49 -  "[" => "{\\isacharbrackleft}" |
    4.50 -  "\\" => "{\\isacharbackslash}" |
    4.51 -  "]" => "{\\isacharbrackright}" |
    4.52 -  "^" => "{\\isacharcircum}" |
    4.53 -  "_" => "{\\isacharunderscore}" |
    4.54 -  "`" => "{\\isacharbackquote}" |
    4.55 -  "{" => "{\\isacharbraceleft}" |
    4.56 -  "|" => "{\\isacharbar}" |
    4.57 -  "}" => "{\\isacharbraceright}" |
    4.58 -  "~" => "{\\isachartilde}" |
    4.59 -  c => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c;
    4.60 +val char_table =
    4.61 +  Symtab.make
    4.62 +   [("!", "{\\isacharbang}"),
    4.63 +    ("\"", "{\\isachardoublequote}"),
    4.64 +    ("#", "{\\isacharhash}"),
    4.65 +    ("$", "{\\isachardollar}"),
    4.66 +    ("%", "{\\isacharpercent}"),
    4.67 +    ("&", "{\\isacharampersand}"),
    4.68 +    ("'", "{\\isacharprime}"),
    4.69 +    ("(", "{\\isacharparenleft}"),
    4.70 +    (")", "{\\isacharparenright}"),
    4.71 +    ("*", "{\\isacharasterisk}"),
    4.72 +    ("+", "{\\isacharplus}"),
    4.73 +    (",", "{\\isacharcomma}"),
    4.74 +    ("-", "{\\isacharminus}"),
    4.75 +    (".", "{\\isachardot}"),
    4.76 +    ("/", "{\\isacharslash}"),
    4.77 +    (":", "{\\isacharcolon}"),
    4.78 +    (";", "{\\isacharsemicolon}"),
    4.79 +    ("<", "{\\isacharless}"),
    4.80 +    ("=", "{\\isacharequal}"),
    4.81 +    (">", "{\\isachargreater}"),
    4.82 +    ("?", "{\\isacharquery}"),
    4.83 +    ("@", "{\\isacharat}"),
    4.84 +    ("[", "{\\isacharbrackleft}"),
    4.85 +    ("\\", "{\\isacharbackslash}"),
    4.86 +    ("]", "{\\isacharbrackright}"),
    4.87 +    ("^", "{\\isacharcircum}"),
    4.88 +    ("_", "{\\isacharunderscore}"),
    4.89 +    ("`", "{\\isacharbackquote}"),
    4.90 +    ("{", "{\\isacharbraceleft}"),
    4.91 +    ("|", "{\\isacharbar}"),
    4.92 +    ("}", "{\\isacharbraceright}"),
    4.93 +    ("~", "{\\isachartilde}")];
    4.94 +
    4.95 +fun output_chr " " = "\\ "
    4.96 +  | output_chr "\n" = "\\isanewline\n"
    4.97 +  | output_chr c =
    4.98 +      (case Symtab.lookup char_table c of
    4.99 +        SOME s => enclose_literal c s
   4.100 +      | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
   4.101  
   4.102  val output_chrs = translate_string output_chr;
   4.103  
   4.104 @@ -78,8 +95,12 @@
   4.105    (case Symbol.decode sym of
   4.106      Symbol.Char s => output_chr s
   4.107    | Symbol.UTF8 s => s
   4.108 -  | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
   4.109 -  | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
   4.110 +  | Symbol.Sym s =>
   4.111 +      if known_sym s then enclose_literal sym (enclose "{\\isasym" "}" s)
   4.112 +      else output_chrs sym
   4.113 +  | Symbol.Ctrl s =>
   4.114 +      if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s
   4.115 +      else output_chrs sym
   4.116    | Symbol.Raw s => s);
   4.117  
   4.118  in
   4.119 @@ -91,9 +112,10 @@
   4.120  val output_syms_antiq =
   4.121    (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
   4.122      | Antiquote.Antiq (ss, _) =>
   4.123 -        enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
   4.124 -    | Antiquote.Open _ => "{\\isaantiqopen}"
   4.125 -    | Antiquote.Close _ => "{\\isaantiqclose}");
   4.126 +        enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
   4.127 +          (output_symbols (map Symbol_Pos.symbol ss))
   4.128 +    | Antiquote.Open _ => enclose_literal "\\<lbrace>" "{\\isaantiqopen}"
   4.129 +    | Antiquote.Close _ => enclose_literal "\\<rbrace>" "{\\isaantiqclose}");
   4.130  
   4.131  end;
   4.132  
   4.133 @@ -110,15 +132,23 @@
   4.134      else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then
   4.135        "\\isakeyword{" ^ output_syms s ^ "}"
   4.136      else if Token.is_kind Token.String tok then
   4.137 -      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
   4.138 +      output_syms s |> enclose
   4.139 +        (enclose_literal "\"" "{\\isachardoublequoteopen}")
   4.140 +        (enclose_literal "\"" "{\\isachardoublequoteclose}")
   4.141      else if Token.is_kind Token.AltString tok then
   4.142 -      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
   4.143 +      output_syms s |> enclose
   4.144 +        (enclose_literal "`" "{\\isacharbackquoteopen}")
   4.145 +        (enclose_literal "`" "{\\isacharbackquoteclose}")
   4.146      else if Token.is_kind Token.Verbatim tok then
   4.147        let
   4.148          val (txt, pos) = Token.source_position_of tok;
   4.149          val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
   4.150          val out = implode (map output_syms_antiq ants);
   4.151 -      in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
   4.152 +      in
   4.153 +        out |> enclose
   4.154 +          (enclose_literal "{*" "{\\isacharverbatimopen}")
   4.155 +          (enclose_literal "*}" "{\\isacharverbatimclose}")
   4.156 +      end
   4.157      else output_syms s
   4.158    end;
   4.159