69288
|
1 |
{- generated by Isabelle -}
|
|
2 |
|
|
3 |
{- Title: Tools/Haskell/Completion.hs
|
|
4 |
Author: Makarius
|
|
5 |
LICENSE: BSD 3-clause (Isabelle)
|
|
6 |
|
|
7 |
Completion of names.
|
|
8 |
|
|
9 |
See also "$ISABELLE_HOME/src/Pure/General/completion.ML".
|
|
10 |
-}
|
|
11 |
|
|
12 |
module Isabelle.Completion (Name, T, names, none, make, encode, reported_text)
|
|
13 |
where
|
|
14 |
|
|
15 |
import qualified Data.List as List
|
|
16 |
|
|
17 |
import Isabelle.Library
|
|
18 |
import qualified Isabelle.Properties as Properties
|
|
19 |
import qualified Isabelle.Markup as Markup
|
|
20 |
import qualified Isabelle.XML.Encode as Encode
|
|
21 |
import qualified Isabelle.XML as XML
|
|
22 |
import qualified Isabelle.YXML as YXML
|
|
23 |
|
|
24 |
|
|
25 |
type Name = (String, (String, String)) -- external name, kind, internal name
|
|
26 |
data T = Completion Properties.T Int [Name] -- position, total length, names
|
|
27 |
|
|
28 |
names :: Int -> Properties.T -> [Name] -> T
|
|
29 |
names limit props names = Completion props (length names) (take limit names)
|
|
30 |
|
|
31 |
none :: T
|
|
32 |
none = names 0 [] []
|
|
33 |
|
|
34 |
make :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> T
|
|
35 |
make limit (name, props) make_names =
|
|
36 |
if name /= "" && name /= "_"
|
|
37 |
then names limit props (make_names $ List.isPrefixOf $ clean_name name)
|
|
38 |
else none
|
|
39 |
|
|
40 |
encode :: T -> XML.Body
|
|
41 |
encode (Completion _ total names) =
|
|
42 |
Encode.pair Encode.int
|
|
43 |
(Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string)))
|
|
44 |
(total, names)
|
|
45 |
|
|
46 |
reported_text :: T -> String
|
|
47 |
reported_text completion@(Completion props total names) =
|
|
48 |
if not (null names) then
|
|
49 |
let markup = Markup.properties props Markup.completion
|
|
50 |
in YXML.string_of $ XML.Elem markup (encode completion)
|
|
51 |
else ""
|