--- a/src/Tools/Haskell/Completion.hs Fri Nov 30 23:30:42 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-{- generated by Isabelle -}
-
-{- Title: Tools/Haskell/Completion.hs
- Author: Makarius
- LICENSE: BSD 3-clause (Isabelle)
-
-Completion of names.
-
-See also "$ISABELLE_HOME/src/Pure/General/completion.ML".
--}
-
-module Isabelle.Completion (
- Name, T, names, none, make, markup_element, markup_report, make_report
- ) where
-
-import qualified Data.List as List
-
-import Isabelle.Library
-import qualified Isabelle.Properties as Properties
-import qualified Isabelle.Markup as Markup
-import qualified Isabelle.XML.Encode as Encode
-import qualified Isabelle.XML as XML
-import qualified Isabelle.YXML as YXML
-
-
-type Name = (String, (String, String)) -- external name, kind, internal name
-data T = Completion Properties.T Int [Name] -- position, total length, names
-
-names :: Int -> Properties.T -> [Name] -> T
-names limit props names = Completion props (length names) (take limit names)
-
-none :: T
-none = names 0 [] []
-
-make :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> T
-make limit (name, props) make_names =
- if name /= "" && name /= "_"
- then names limit props (make_names $ List.isPrefixOf $ clean_name name)
- else none
-
-markup_element :: T -> (Markup.T, XML.Body)
-markup_element (Completion props total names) =
- if not (null names) then
- let
- markup = Markup.properties props Markup.completion
- body =
- Encode.pair Encode.int
- (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string)))
- (total, names)
- in (markup, body)
- else (Markup.empty, [])
-
-markup_report :: [T] -> String
-markup_report [] = ""
-markup_report elems =
- YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
-
-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]