src/Tools/Haskell/Completion.hs

tuned signature;

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