Changeset 12769

Timestamp:

31.10.2009 15:48:41 (3 weeks ago)

Author:

maeder

Message:

replace ' ' char to avoid duplicate axioms

Files:

• trunk/Isabelle/Translate.hs (modified) (6 diffs)

trunk/Isabelle/Translate.hs

@@ -18 +18 @@
     , getConstIsaToks ) where
 
+import Common.AS_Annotation
+import Common.GlobalAnnotations
 import Common.Id
 import Common.ProofUtils
-import Common.GlobalAnnotations
-import Common.AS_Annotation
+import Common.Utils
+import qualified Common.Lib.Rel as Rel
 
 import qualified Data.Map as Map
 import qualified Data.Set as Set
-import qualified Common.Lib.Rel as Rel
+
 import Data.Char
+import Data.Maybe
 import Data.List
 
@@ -100 +103 @@
     atoks@(hd : tl) = getAltTokenList newPlace over i thy
     compoundToks = map (: []) ",[]{}"
-    convert = \ Token { tokStr = s } ->
+    convert Token { tokStr = s } =
       if elem s $ newPlace : compoundToks then s else br ++ quote s
     tts = concatMap convert tl
@@ -146 +149 @@
 mkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set.Set String
             -> VName
-mkIsaConstT prd ga n ide = mkIsaConstVName 0 showIsaConstT prd ga n ide
+mkIsaConstT = mkIsaConstVName 0 showIsaConstT
 
 mkIsaConstVName :: Int -> (Id -> BaseSig -> String) -> Bool -> GlobalAnnos
@@ -180 +183 @@
 
 getConstIsaToksAux :: Id -> Int -> BaseSig -> Set.Set String
-getConstIsaToksAux ide i thy =
+getConstIsaToksAux ide i =
    foldr (Set.insert . tokStr)
-             Set.empty $ getAltTokenList "" i ide thy
+             Set.empty . getAltTokenList "" i ide
 
 transIsaStringT :: Map.Map BaseSig (Set.Set String) -> BaseSig
                 -> String -> String
 transIsaStringT m i s = let t = transStringAux False s in
-  if Set.member t $ maybe (error "Isabelle.transIsaStringT") id
+  if Set.member t $ fromMaybe (error "Isabelle.transIsaStringT")
          $ Map.lookup i m
-  then transIsaStringT m i $ "_" ++ s else t
+  then transIsaStringT m i $ '_' : s else t
 
 transConstStringT :: BaseSig -> String -> String
@@ -217 +220 @@
     c : s -> let l = replaceChar1 c in
              (if isDigit c || elem c "_'" then [x, c]
-             else l) ++ concatMap replaceChar1 s
+             else l) ++ concatMap replaceChar1
+        (if b then replace "' '" "'Space'" s else s)
 
 -- | injective replacement of special characters
@@ -224 +228 @@
 replaceChar c = if isIsaChar c then [c] else let n = ord c in
     if n <= 32 || n >= 127 && n < 160 || n > 255 then "Slash_" ++ show n
-    else maybe (error "Isabelle.replaceChar") id $ Map.lookup c charMap
+    else fromMaybe (error "Isabelle.replaceChar") $ Map.lookup c charMap