Allow for customizing the "input mode" toolbar
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
14b63fccc2
commit
b6569d8ca0
88
src/Main.elm
88
src/Main.elm
|
|
@ -13,6 +13,7 @@ import Bergamot.Latex exposing (..)
|
|||
import Bergamot.ObjectLanguage exposing (topLevelExpr, exprToTerm)
|
||||
import Bergamot.Utils exposing (..)
|
||||
import Json.Encode
|
||||
import Json.Decode exposing (string, field, list, oneOf, succeed, fail)
|
||||
import Maybe
|
||||
import Tuple
|
||||
|
||||
|
|
@ -32,13 +33,7 @@ tabEq t1 t2 =
|
|||
type EditMode
|
||||
= Query
|
||||
| Syntax
|
||||
|
||||
editModeEq : EditMode -> EditMode -> Bool
|
||||
editModeEq m1 m2 =
|
||||
case (m1, m2) of
|
||||
(Query, Query) -> True
|
||||
(Syntax, Syntax) -> True
|
||||
_ -> False
|
||||
| Custom String
|
||||
|
||||
type ResultMode
|
||||
= Conclusion
|
||||
|
|
@ -57,20 +52,57 @@ type alias Model =
|
|||
, inputProgram : String
|
||||
, tab : Tab
|
||||
, query : String
|
||||
, editMode : EditMode
|
||||
, inputModes : List (String, EditMode)
|
||||
, inputMode : Int
|
||||
, resultMode : ResultMode
|
||||
}
|
||||
type alias Flags = { renderRules: String, inputRules: String, rules: String, query: String }
|
||||
type alias Flags =
|
||||
{ renderRules : String
|
||||
, inputRules : String
|
||||
, rules : String
|
||||
, query : String
|
||||
, inputModes : Json.Decode.Value
|
||||
}
|
||||
type Msg
|
||||
= SetProgram String
|
||||
| SetRenderProgram String
|
||||
| SetQuery String
|
||||
| SetTab Tab
|
||||
| SetEditMode EditMode
|
||||
| SetInputMode Int
|
||||
| SetResultMode ResultMode
|
||||
|
||||
decodeInputModes: Json.Decode.Value -> List (String, EditMode)
|
||||
decodeInputModes val =
|
||||
let
|
||||
exactString s1 v =
|
||||
string
|
||||
|> Json.Decode.andThen (\s2 -> if s1 == s2
|
||||
then succeed v
|
||||
else Json.Decode.fail "did not match expected string")
|
||||
editModeDecoder = oneOf
|
||||
[ exactString "query" Query
|
||||
, exactString "syntax" Syntax
|
||||
, field "custom" string |> Json.Decode.map Custom
|
||||
]
|
||||
decoder = Json.Decode.keyValuePairs editModeDecoder
|
||||
in
|
||||
case Json.Decode.decodeValue decoder val of
|
||||
Ok l -> l
|
||||
Err _ -> [("Query", Query), ("Language Term", Syntax)]
|
||||
|
||||
init : Flags -> (Model, Cmd Msg)
|
||||
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, inputProgram = fs.inputRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none)
|
||||
init fs =
|
||||
( { program = fs.rules
|
||||
, renderProgram = fs.renderRules
|
||||
, inputProgram = fs.inputRules
|
||||
, query = fs.query
|
||||
, tab = Rendered
|
||||
, inputModes = decodeInputModes fs.inputModes
|
||||
, inputMode = 0
|
||||
, resultMode = Conclusion
|
||||
}
|
||||
, Cmd.none
|
||||
)
|
||||
|
||||
viewSection : String -> Html Msg -> Html Msg
|
||||
viewSection name content =
|
||||
|
|
@ -83,23 +115,23 @@ viewTab tab editor metaEditor rendered =
|
|||
MetaEditor -> metaEditor
|
||||
Rendered -> rendered
|
||||
|
||||
viewSelector : (a -> a -> Bool) -> (a -> Msg) -> a -> List (a, String) -> Html Msg
|
||||
viewSelector : (Int -> a -> b -> Bool) -> (Int -> a -> Msg) -> b -> List (a, String) -> Html Msg
|
||||
viewSelector eq mkMsg mode modeNames =
|
||||
Html.div [ class "bergamot-selector" ] <|
|
||||
List.map (\(modep, name) ->
|
||||
List.indexedMap (\idx (modep, name) ->
|
||||
Html.button
|
||||
[ classList [("active", eq mode modep)]
|
||||
, onClick (mkMsg modep)
|
||||
[ classList [("active", eq idx modep mode)]
|
||||
, onClick (mkMsg idx modep)
|
||||
] [ Html.text name ]) modeNames
|
||||
|
||||
viewTabSelector : Tab -> List (Tab, String) -> Html Msg
|
||||
viewTabSelector = viewSelector tabEq SetTab
|
||||
viewTabSelector = viewSelector (\_ -> tabEq) (\_ -> SetTab)
|
||||
|
||||
viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
|
||||
viewEditModeSelector = viewSelector editModeEq SetEditMode
|
||||
viewInputModeSelector : Int -> List (EditMode, String) -> Html Msg
|
||||
viewInputModeSelector = viewSelector (\i _ idx -> i == idx) (\idx _ -> SetInputMode idx)
|
||||
|
||||
viewResultModeSelector : ResultMode -> List (ResultMode, String) -> Html Msg
|
||||
viewResultModeSelector = viewSelector resultModeEq SetResultMode
|
||||
viewResultModeSelector = viewSelector (\_ -> resultModeEq) (\_ -> SetResultMode)
|
||||
|
||||
viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
|
||||
viewRule env r = renderRuleViaRules env r
|
||||
|
|
@ -130,6 +162,7 @@ type Error
|
|||
| BadProg
|
||||
| BadRenderProg
|
||||
| FailedRender
|
||||
| InvalidInputMode
|
||||
| Silent
|
||||
|
||||
combineTwoResults : (a -> b -> Result Error c) -> Result Error a -> Result Error b -> Result Error c
|
||||
|
|
@ -151,6 +184,7 @@ errorToString err =
|
|||
BadProg -> "Unable to parse rules"
|
||||
BadRenderProg -> "Unable to parse rendering rules"
|
||||
FailedRender -> "Unable to render terms using provided rendering rules"
|
||||
InvalidInputMode -> "Invalid edit mode specified"
|
||||
Silent -> ""
|
||||
|
||||
viewError : Error -> Html Msg
|
||||
|
|
@ -170,6 +204,13 @@ viewOrError r =
|
|||
Err e -> Html.div [] [ viewError e ] -- The div wrapper is needed because Elm has a bug?
|
||||
Ok html -> html
|
||||
|
||||
getEditMode : Int -> List (String, EditMode) -> Result Error EditMode
|
||||
getEditMode i l =
|
||||
case l of
|
||||
[] -> Err InvalidInputMode
|
||||
((_, editMode) :: xs) ->
|
||||
if i == 0 then Ok editMode else getEditMode (i - 1) xs
|
||||
|
||||
proofGoal : EditMode -> String -> String -> Result Error (Term Metavariable)
|
||||
proofGoal editMode inputProgs querys =
|
||||
if querys == ""
|
||||
|
|
@ -196,6 +237,7 @@ proofGoal editMode inputProgs querys =
|
|||
_ -> Err NoConversionResults
|
||||
(_, Nothing) -> Err BadObjectTerm
|
||||
(Nothing, _) -> Err BadInputProg
|
||||
Custom _ -> Err BadInputProg
|
||||
|
||||
progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv)
|
||||
progAndRenderProg progs renderProgs =
|
||||
|
|
@ -227,13 +269,15 @@ viewProofTree resultMode query (prog, renderProg) =
|
|||
view : Model -> Html Msg
|
||||
view m =
|
||||
let
|
||||
termOrErr = proofGoal m.editMode m.inputProgram m.query
|
||||
mode = getEditMode m.inputMode m.inputModes
|
||||
termOrErr = mode |> Result.andThen (\editMode -> proofGoal editMode m.inputProgram m.query)
|
||||
progsOrErr = progAndRenderProg m.program m.renderProgram
|
||||
proofTreeOrErr = combineTwoResults (viewProofTree m.resultMode) termOrErr progsOrErr
|
||||
in
|
||||
Html.div [ class "bergamot-root" ]
|
||||
[ viewSection "Input" <| Html.div [] <|
|
||||
[ viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
|
||||
[ viewInputModeSelector m.inputMode <|
|
||||
List.map (\(a, b) -> (b, a)) m.inputModes
|
||||
, Html.input [ type_ "text", onInput SetQuery, value m.query ] []
|
||||
] ++
|
||||
viewIfError termOrErr
|
||||
|
|
@ -258,7 +302,7 @@ update msg m =
|
|||
SetRenderProgram prog -> ({ m | renderProgram = prog }, Cmd.none)
|
||||
SetQuery query -> ({ m | query = query }, Cmd.none)
|
||||
SetTab tab -> ({ m | tab = tab }, Cmd.none)
|
||||
SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
|
||||
SetInputMode mode -> ({ m | inputMode = mode }, Cmd.none)
|
||||
SetResultMode mode -> ({ m | resultMode = mode }, Cmd.none)
|
||||
|
||||
subscriptions : Model -> Sub Msg
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user