Copying with tokens

Coping text "as Unicode" (Tokens -> Copy as Unicode) makes it readable in Unicode editors, web pages etc. Here's an example:

text {* "weak" typing relation *}

inductive typing :: "cxt⇒llam⇒ty⇒bool" (" _ ⊢ _ : _ " [60,60,60] 60) where t_lPar[intro]: "⟦valid Γ; (x,T)∈set Γ⟧⟹ Γ ⊢ lPar x : T" | t_lApp[intro]: "⟦Γ ⊢ t1 : T1→T2; Γ ⊢ t2 : T1⟧⟹ Γ ⊢ lApp t1 t2 : T2" | t_lLam[intro]: "⟦x♯t; (x,T1)#Γ ⊢ freshen t x : T2⟧⟹ Γ ⊢ lLam t : T1→T2"

With plain "ASCII" copy (Edit -> Copy) this text looks like this:

text {* "weak" typing relation *}

inductive typing :: "cxt\llam\ty\bool" (" _ \ _ : _ " [60,60,60] 60) where t_lPar[intro]: "\valid \; (x,T)\set \\\ \ \ lPar x : T" | t_lApp[intro]: "\\ \ t1 : T1\T2; \ \ t2 : T1\\ \ \ lApp t1 t2 : T2" | t_lLam[intro]: "\x\t; (x,T1)#\ \ freshen t x : T2\\ \ \ lLam t : T1\T2"

Unreadable!

The copy conversion won't work where the text compositions contain layout information. Also, control tokens will still be copied, so subscripts are not ideal, e.g.

definition
  map_le :: "('a &#8640; 'b) => ('a &#8640; 'b) &#8640; bool"  (infix "&#8838;\<^sub>m" 50) where
  "(m\<^isub>1 &#8838;\<^sub>m m\<^isub>2) = (&#8704;a &#8712; dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)"

Paste

Topic revision: r1 - 21 Jul 2008 - 11:10:32 - DavidAspinall
 
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies