src/Tools/Haskell/Completion.hs

more Haskell operations;
more accurate exports;
tuned;

{- 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 ""