# HG changeset patch # User wenzelm # Date 1542027753 -3600 # Node ID 4c3704ecb0e62b184fe094b2cf724e42d6b43fd4 # Parent 0fde0dca6744bb8a3d00862305db99ee6c9dff25 more Haskell operations; more accurate exports; tuned; diff -r 0fde0dca6744 -r 4c3704ecb0e6 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 "" diff -r 0fde0dca6744 -r 4c3704ecb0e6 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Mon Nov 12 11:41:11 2018 +0100 +++ b/src/Tools/Haskell/Haskell.thy Mon Nov 12 14:02:33 2018 +0100 @@ -44,7 +44,7 @@ fold, fold_rev, single, map_index, get_index, - quote, trim_line) + quote, trim_line, clean_name) where import Data.Maybe @@ -116,6 +116,9 @@ '\n' : '\r' : rest -> reverse rest '\n' : rest -> reverse rest _ -> line + +clean_name :: String -> String +clean_name = reverse #> dropWhile (== '_') #> reverse \ generate_haskell_file "Value.hs" = \ @@ -246,6 +249,8 @@ nameN, name, xnameN, xname, kindN, + completionN, completion, no_completionN, no_completion, + lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position, markupN, consistentN, unbreakableN, indentN, widthN, @@ -317,6 +322,15 @@ kindN = \Markup.kindN\ +{- completion -} + +completionN :: String; completion :: T +(completionN, completion) = markup_elem \Markup.completionN\ + +no_completionN :: String; no_completion :: T +(no_completionN, no_completion) = markup_elem \Markup.no_completionN\ + + {- position -} lineN, end_lineN :: String @@ -526,6 +540,58 @@ no_output = ("", "") \ +generate_haskell_file "Completion.hs" = \ +{- Title: Tools/Haskell/Completion.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Completion of names. + +See also \<^file>\$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 "" +\ + generate_haskell_file "File.hs" = \ {- Title: Tools/Haskell/File.hs Author: Makarius @@ -837,6 +903,134 @@ variant _ _ = err_body \ +generate_haskell_file "YXML.hs" = \ +{- Title: Tools/Haskell/YXML.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Efficient text representation of XML trees. Suitable for direct +inlining into plain text. + +See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\. +-} + +module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup, + buffer_body, buffer, string_of_body, string_of, parse_body, parse) +where + +import qualified Data.Char as Char +import qualified Data.List as List + +import Isabelle.Library +import qualified Isabelle.Markup as Markup +import qualified Isabelle.XML as XML +import qualified Isabelle.Buffer as Buffer + + +{- markers -} + +charX, charY :: Char +charX = Char.chr 5 +charY = Char.chr 6 + +strX, strY, strXY, strXYX :: String +strX = [charX] +strY = [charY] +strXY = strX ++ strY +strXYX = strXY ++ strX + +detect :: String -> Bool +detect = any (\c -> c == charX || c == charY) + + +{- output -} + +output_markup :: Markup.T -> Markup.Output +output_markup markup@(name, atts) = + if Markup.is_empty markup then Markup.no_output + else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX) + +buffer_attrib (a, x) = + Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x + +buffer_body :: XML.Body -> Buffer.T -> Buffer.T +buffer_body = fold buffer + +buffer :: XML.Tree -> Buffer.T -> Buffer.T +buffer (XML.Elem (name, atts) ts) = + Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #> + buffer_body ts #> + Buffer.add strXYX +buffer (XML.Text s) = Buffer.add s + +string_of_body :: XML.Body -> String +string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content + +string_of :: XML.Tree -> String +string_of = string_of_body . single + + +{- parse -} + +-- split: fields or non-empty tokens + +split :: Bool -> Char -> String -> [String] +split _ _ [] = [] +split fields sep str = splitting str + where + splitting rest = + case span (/= sep) rest of + (_, []) -> cons rest [] + (prfx, _ : rest') -> cons prfx (splitting rest') + cons item = if fields || not (null item) then (:) item else id + + +-- structural errors + +err msg = error ("Malformed YXML: " ++ msg) +err_attribute = err "bad attribute" +err_element = err "bad element" +err_unbalanced "" = err "unbalanced element" +err_unbalanced name = err ("unbalanced element " ++ quote name) + + +-- stack operations + +add x ((elem, body) : pending) = (elem, x : body) : pending + +push "" _ _ = err_element +push name atts pending = ((name, atts), []) : pending + +pop ((("", _), _) : _) = err_unbalanced "" +pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending + + +-- parsing + +parse_attrib s = + case List.elemIndex '=' s of + Just i | i > 0 -> (take i s, drop (i + 1) s) + _ -> err_attribute + +parse_chunk ["", ""] = pop +parse_chunk ("" : name : atts) = push name (map parse_attrib atts) +parse_chunk txts = fold (add . XML.Text) txts + +parse_body :: String -> XML.Body +parse_body source = + case fold parse_chunk chunks [(("", []), [])] of + [(("", _), result)] -> reverse result + ((name, _), _) : _ -> err_unbalanced name + where chunks = split False charX source |> map (split True charY) + +parse :: String -> XML.Tree +parse source = + case parse_body source of + [result] -> result + [] -> XML.Text "" + _ -> err "multiple results" +\ + generate_haskell_file "Pretty.hs" = \ {- Title: Tools/Haskell/Pretty.hs Author: Makarius @@ -991,134 +1185,6 @@ big_list name prts = block (fbreaks (str name : prts)) \ -generate_haskell_file "YXML.hs" = \ -{- Title: Tools/Haskell/YXML.hs - Author: Makarius - LICENSE: BSD 3-clause (Isabelle) - -Efficient text representation of XML trees. Suitable for direct -inlining into plain text. - -See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\. --} - -module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup, - buffer_body, buffer, string_of_body, string_of, parse_body, parse) -where - -import qualified Data.Char as Char -import qualified Data.List as List - -import Isabelle.Library -import qualified Isabelle.Markup as Markup -import qualified Isabelle.XML as XML -import qualified Isabelle.Buffer as Buffer - - -{- markers -} - -charX, charY :: Char -charX = Char.chr 5 -charY = Char.chr 6 - -strX, strY, strXY, strXYX :: String -strX = [charX] -strY = [charY] -strXY = strX ++ strY -strXYX = strXY ++ strX - -detect :: String -> Bool -detect = any (\c -> c == charX || c == charY) - - -{- output -} - -output_markup :: Markup.T -> Markup.Output -output_markup markup@(name, atts) = - if Markup.is_empty markup then Markup.no_output - else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX) - -buffer_attrib (a, x) = - Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x - -buffer_body :: XML.Body -> Buffer.T -> Buffer.T -buffer_body = fold buffer - -buffer :: XML.Tree -> Buffer.T -> Buffer.T -buffer (XML.Elem (name, atts) ts) = - Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #> - buffer_body ts #> - Buffer.add strXYX -buffer (XML.Text s) = Buffer.add s - -string_of_body :: XML.Body -> String -string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content - -string_of :: XML.Tree -> String -string_of = string_of_body . single - - -{- parse -} - --- split: fields or non-empty tokens - -split :: Bool -> Char -> String -> [String] -split _ _ [] = [] -split fields sep str = splitting str - where - splitting rest = - case span (/= sep) rest of - (_, []) -> cons rest [] - (prfx, _ : rest') -> cons prfx (splitting rest') - cons item = if fields || not (null item) then (:) item else id - - --- structural errors - -err msg = error ("Malformed YXML: " ++ msg) -err_attribute = err "bad attribute" -err_element = err "bad element" -err_unbalanced "" = err "unbalanced element" -err_unbalanced name = err ("unbalanced element " ++ quote name) - - --- stack operations - -add x ((elem, body) : pending) = (elem, x : body) : pending - -push "" _ _ = err_element -push name atts pending = ((name, atts), []) : pending - -pop ((("", _), _) : _) = err_unbalanced "" -pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending - - --- parsing - -parse_attrib s = - case List.elemIndex '=' s of - Just i | i > 0 -> (take i s, drop (i + 1) s) - _ -> err_attribute - -parse_chunk ["", ""] = pop -parse_chunk ("" : name : atts) = push name (map parse_attrib atts) -parse_chunk txts = fold (add . XML.Text) txts - -parse_body :: String -> XML.Body -parse_body source = - case fold parse_chunk chunks [(("", []), [])] of - [(("", _), result)] -> reverse result - ((name, _), _) : _ -> err_unbalanced name - where chunks = split False charX source |> map (split True charY) - -parse :: String -> XML.Tree -parse source = - case parse_body source of - [result] -> result - [] -> XML.Text "" - _ -> err "multiple results" -\ - generate_haskell_file "Term.hs" = \ {- Title: Tools/Haskell/Term.hs Author: Makarius diff -r 0fde0dca6744 -r 4c3704ecb0e6 src/Tools/Haskell/Library.hs --- a/src/Tools/Haskell/Library.hs Mon Nov 12 11:41:11 2018 +0100 +++ b/src/Tools/Haskell/Library.hs Mon Nov 12 14:02:33 2018 +0100 @@ -16,7 +16,7 @@ fold, fold_rev, single, map_index, get_index, - quote, trim_line) + quote, trim_line, clean_name) where import Data.Maybe @@ -88,3 +88,6 @@ '\n' : '\r' : rest -> reverse rest '\n' : rest -> reverse rest _ -> line + +clean_name :: String -> String +clean_name = reverse #> dropWhile (== '_') #> reverse diff -r 0fde0dca6744 -r 4c3704ecb0e6 src/Tools/Haskell/Markup.hs --- a/src/Tools/Haskell/Markup.hs Mon Nov 12 11:41:11 2018 +0100 +++ b/src/Tools/Haskell/Markup.hs Mon Nov 12 14:02:33 2018 +0100 @@ -14,6 +14,8 @@ nameN, name, xnameN, xname, kindN, + completionN, completion, no_completionN, no_completion, + lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position, markupN, consistentN, unbreakableN, indentN, widthN, @@ -85,6 +87,15 @@ kindN = "kind" +{- completion -} + +completionN :: String; completion :: T +(completionN, completion) = markup_elem "completion" + +no_completionN :: String; no_completion :: T +(no_completionN, no_completion) = markup_elem "no_completion" + + {- position -} lineN, end_lineN :: String diff -r 0fde0dca6744 -r 4c3704ecb0e6 src/Tools/Haskell/haskell.ML --- a/src/Tools/Haskell/haskell.ML Mon Nov 12 11:41:11 2018 +0100 +++ b/src/Tools/Haskell/haskell.ML Mon Nov 12 14:02:33 2018 +0100 @@ -52,6 +52,8 @@ \<^path>\Buffer.hs\, \<^path>\Properties.hs\, \<^path>\Markup.hs\, + \<^path>\Completion.hs\, + \<^path>\File.hs\, \<^path>\XML.hs\, \<^path>\XML/Encode.hs\, \<^path>\XML/Decode.hs\,