view Paper/escape_agda.rb @ 8:83d000399c9d

fix invisible char
author ryokka
date Tue, 18 Dec 2018 04:08:28 +0900
parents 493983f2c9db
children
line wrap: on
line source

#!/usr/bin/env ruby

Suffix     = '.agda.replaced'
EscapeChar = '@'
FileName   = ARGV.first

ReplaceTable = {
  '->' => 'rightarrow',
  '⊔'  => 'sqcup',
  '∷' => 'text{::}',
  '∙'  => 'circ',
  '≡' => 'equiv',
  '×' => 'times',
  '⟨'  => 'langle',
  '⟩'  => 'rangle',
  '₁' => 'text{1}',
  'ℕ' => 'mathbb{N}',
  '∎'  => 'blacksquare',
  'λ' => 'lambda',
  '∧' => 'wedge',
  '⇒' => 'Rightarrow',
  '¬' => 'neg',
  '≤' => 'leq',
  '⊥' => 'bot',
}

code = File.read(FileName)
ReplaceTable.each do |k, v|
  escaped_str = EscapeChar + "$\\#{v}$" + EscapeChar
  code = code.gsub(k, escaped_str)
end

File.write(FileName.sub(/.agda$/, Suffix), code)