src/Tools/Haskell/Haskell.thy

 
 theory Haskell
   imports Pure
 begin
 
-generate_file "Library.hs" = \<open>
+generate_file "Isabelle/Library.hs" = \<open>
 {-  Title:      Tools/Haskell/Library.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Basic library of Isabelle idioms.

 
 clean_name :: String -> String
 clean_name = reverse #> dropWhile (== '_') #> reverse
 \<close>
 
-generate_file "Value.hs" = \<open>
+generate_file "Isabelle/Value.hs" = \<open>
 {-  Title:      Haskell/Tools/Value.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Plain values, represented as string.

 
 parse_real :: String -> Maybe Double
 parse_real = Read.readMaybe
 \<close>
 
-generate_file "Buffer.hs" = \<open>
+generate_file "Isabelle/Buffer.hs" = \<open>
 {-  Title:      Tools/Haskell/Buffer.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Efficient text buffers.

 
 content :: T -> String
 content (Buffer xs) = concat (reverse xs)
 \<close>
 
-generate_file "Properties.hs" = \<open>
+generate_file "Isabelle/Properties.hs" = \<open>
 {-  Title:      Tools/Haskell/Properties.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Property lists.

 remove name props =
   if defined props name then filter (\(a, _) -> a /= name) props
   else props
 \<close>
 
-generate_file "Markup.hs" = \<open>
+generate_file "Isabelle/Markup.hs" = \<open>
 {-  Title:      Haskell/Tools/Markup.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Quasi-abstract markup elements.

 
 no_output :: Output
 no_output = ("", "")
 \<close>
 
-generate_file "Completion.hs" = \<open>
+generate_file "Isabelle/Completion.hs" = \<open>
 {-  Title:      Tools/Haskell/Completion.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Completion of names.

 make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String
 make_report limit name_props make_names =
   markup_report [make limit name_props make_names]
 \<close>
 
-generate_file "File.hs" = \<open>
+generate_file "Isabelle/File.hs" = \<open>
 {-  Title:      Tools/Haskell/File.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 File-system operations.

 append :: IO.FilePath -> String -> IO ()
 append path s =
   IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s)
 \<close>
 
-generate_file "XML.hs" = \<open>
+generate_file "Isabelle/XML.hs" = \<open>
 {-  Title:      Tools/Haskell/XML.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Untyped XML trees and representation of ML values.

         unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
 
       show_text = concatMap encode
 \<close>
 
-generate_file "XML/Encode.hs" = \<open>
+generate_file "Isabelle/XML/Encode.hs" = \<open>
 {-  Title:      Tools/Haskell/XML/Encode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 XML as data representation language.

 
 variant :: [V a] -> T a
 variant fs x = [tagged (the (get_index (\f -> f x) fs))]
 \<close>
 
-generate_file "XML/Decode.hs" = \<open>
+generate_file "Isabelle/XML/Decode.hs" = \<open>
 {-  Title:      Tools/Haskell/XML/Decode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 XML as data representation language.

 variant fs [t] = (fs !! tag) (xs, ts)
   where (tag, (xs, ts)) = tagged t
 variant _ _ = err_body
 \<close>
 
-generate_file "YXML.hs" = \<open>
+generate_file "Isabelle/YXML.hs" = \<open>
 {-  Title:      Tools/Haskell/YXML.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Efficient text representation of XML trees.  Suitable for direct

     [result] -> result
     [] -> XML.Text ""
     _ -> err "multiple results"
 \<close>
 
-generate_file "Pretty.hs" = \<open>
+generate_file "Isabelle/Pretty.hs" = \<open>
 {-  Title:      Tools/Haskell/Pretty.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Generic pretty printing module.

 
 big_list :: String -> [T] -> T
 big_list name prts = block (fbreaks (str name : prts))
 \<close>
 
-generate_file "Term.hs" = \<open>
+generate_file "Isabelle/Term.hs" = \<open>
 {-  Title:      Tools/Haskell/Term.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 Lambda terms, types, sorts.

   | Abs (String, Typ, Term)
   | App (Term, Term)
   deriving Show
 \<close>
 
-generate_file "Term_XML/Encode.hs" = \<open>
+generate_file "Isabelle/Term_XML/Encode.hs" = \<open>
 {-  Title:      Tools/Haskell/Term_XML/Encode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 XML data representation of lambda terms.

     \case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
     \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
     \case { App a -> Just ([], pair term term a); _ -> Nothing }]
 \<close>
 
-generate_file "Term_XML/Decode.hs" = \<open>
+generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
 {-  Title:      Tools/Haskell/Term_XML/Decode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
 XML data representation of lambda terms.