src/Tools/Haskell/Completion.hs

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Haskell/Completion.hs	Mon Nov 12 14:02:33 2018 +0100
@@ -0,0 +1,51 @@
+{- 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, encode, reported_text)
+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
+
+encode :: T -> XML.Body
+encode (Completion _ total names) =
+  Encode.pair Encode.int
+    (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string)))
+    (total, names)
+
+reported_text :: T -> String
+reported_text completion@(Completion props total names) =
+  if not (null names) then
+    let markup = Markup.properties props Markup.completion
+    in YXML.string_of $ XML.Elem markup (encode completion)
+  else ""