@@ -45,6 +45,7 @@ <h2>Agda mode</h2>
4545 < select id ="mode-select " data-option-key ="mode ">
4646 < option value ="agda "> Agda</ option >
4747 < option value ="haskell "> Haskell</ option >
48+ < option value ="python "> Python</ option >
4849 </ select >
4950
5051 < label for ="keymap-select "> KeyMap:</ label >
@@ -60,20 +61,58 @@ <h2>Agda mode</h2>
6061< script src ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.44.0/addon/mode/simple.min.js "> </ script >
6162< script src ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.44.0/addon/hint/show-hint.min.js "> </ script >
6263< script src ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.44.0/mode/haskell/haskell.min.js "> </ script >
64+ < script src ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.44.0/mode/python/python.min.js "> </ script >
6365< script src ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.44.0/keymap/vim.min.js "> </ script >
6466< script src ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.44.0/keymap/emacs.min.js "> </ script >
6567< script src ="https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.44.0/keymap/sublime.min.js "> </ script >
6668< script src ="agda.js "> </ script >
6769< script >
70+ const autocompleteKeyMap = {
71+ "\\" : function ( cm ) {
72+ cm . replaceSelection ( "\\" ) ;
73+ cm . execCommand ( "autocomplete" ) ;
74+ } ,
75+ } ;
76+ const hintOptions = {
77+ extraKeys : {
78+ // Complete with selected and insert space.
79+ Space : function ( cm ) {
80+ const cA = cm . state . completionActive ;
81+ if ( cA ) {
82+ cA . widget . pick ( ) ;
83+ cm . replaceSelection ( " " ) ;
84+ }
85+ } ,
86+ } ,
87+ // Use custom `closeCharacters` to allow text with ()[]{};:>,
88+ // Note that this isn't documented.
89+ closeCharacters : / [ \s ] / ,
90+ // Disable auto completing even if there's only one choice.
91+ completeSingle : false ,
92+ } ;
93+
94+ // hook to only enable completion in agda mode
95+ function setOption ( editor , key , value ) {
96+ if ( key === "mode" ) {
97+ if ( value === "agda" ) {
98+ editor . addKeyMap ( autocompleteKeyMap ) ;
99+ editor . setOption ( "hintOptions" , hintOptions ) ;
100+ } else {
101+ editor . removeKeyMap ( autocompleteKeyMap ) ;
102+ editor . setOption ( "hintOptions" , undefined ) ;
103+ }
104+ }
105+ editor . setOption ( key , value ) ;
106+ }
107+
68108 const editor = CodeMirror . fromTextArea ( document . getElementById ( "code" ) , {
69- mode : "agda" ,
70109 lineNumbers : true ,
71110 theme : "base16-dark" ,
72111 keyMap : "default" ,
73112 } ) ;
74-
113+ setOption ( editor , "mode" , "agda" ) ;
75114 document . getElementById ( "selects" ) . addEventListener ( "change" , function ( e ) {
76- editor . setOption ( e . target . dataset . optionKey , e . target . value ) ;
115+ setOption ( editor , e . target . dataset . optionKey , e . target . value ) ;
77116 e . stopPropagation ( ) ;
78117 } ) ;
79118</ script >
0 commit comments