226
227
(agda2-load "\C-c\C-l" (global) "Load")
227
228
(agda2-load "\C-c\C-x\C-l")
228
229
(agda2-compile "\C-c\C-x\C-c" (global) "Compile")
229
(agda2-text-state "\C-c\C-x\C-d" (global) "Deactivate Agda")
230
230
(agda2-quit "\C-c\C-x\C-q" (global) "Quit")
231
231
(agda2-restart "\C-c\C-x\C-r" (global) "Restart")
232
(agda2-remove-annotations "\C-c\C-x\C-d" (global) "Remove goals and highlighting (\"deactivate\")")
232
233
(agda2-display-implicit-arguments "\C-c\C-x\C-h" (global) "Toggle display of hidden arguments")
233
(agda2-highlight-reload-or-clear "\C-c\C-x\C-s" (global) "Reload syntax highlighting information")
234
234
(agda2-show-constraints ,(kbd "C-c C-=") (global) "Show constraints")
235
235
(agda2-solveAll ,(kbd "C-c C-s") (global) "Solve constraints")
236
236
(agda2-show-goals ,(kbd "C-c C-?") (global) "Show goals")
328
329
(modify-coding-system-alist 'file "\\.l?agda\\'" 'utf-8)
330
331
(define-derived-mode agda2-mode nil "Agda"
331
"Major mode for agda files.
333
Note that when this mode is activated the default font of the
334
current frame is changed to the fontset `agda2-fontset-name'.
335
The reason is that Agda programs often use mathematical symbols
336
and other Unicode characters, so we try to provide a suitable
337
default font setting, which can display many of the characters
338
encountered. If you prefer to use your own settings, set
339
`agda2-fontset-name' to nil.
332
"Major mode for Agda files.
334
The following paragraph does not apply to Emacs 23.
336
Note that when this mode is activated the default font of the
337
current frame is changed to the fontset `agda2-fontset-name'.
338
The reason is that Agda programs often use mathematical symbols
339
and other Unicode characters, so we try to provide a suitable
340
default font setting, which can display many of the characters
341
encountered. If you prefer to use your own settings, set
342
`agda2-fontset-name' to nil.
341
344
Special commands:
342
345
\\{agda2-mode-map}"
353
356
(set-frame-font agda2-fontset-name)
354
357
(error (error "Unable to change the font; change agda2-fontset-name or tweak agda2-fontset-spec-of-fontset-agda2"))))
355
358
(agda2-indent-setup)
359
;; If GHCi is not running syntax highlighting does not work properly.
360
(unless (eq 'run (agda2-process-status))
356
362
(agda2-highlight-setup)
357
363
(agda2-highlight-reload)
358
364
(agda2-comments-and-paragraphs-setup)
359
365
(force-mode-line-update)
360
366
;; Protect global value of default-input-method from set-input-method.
361
367
(make-local-variable 'default-input-method)
362
(set-input-method "Agda"))
368
(set-input-method "Agda")
369
;; Highlighting is removed when we switch from the Agda mode. Use
370
;; case: When a file M.lagda with a local variables list including
371
;; "mode: latex" is loaded chances are that the Agda mode is
372
;; activated before the LaTeX mode, and the LaTeX mode does not seem
373
;; to remove the text properties set by the Agda mode.
374
(add-hook (make-local-variable 'change-major-mode-hook)
375
'agda2-remove-annotations))
364
377
(defun agda2-restart ()
365
378
"Kill and restart the *ghci* buffer and load `agda2-toplevel-module'."
384
397
(set-buffer-file-coding-system 'utf-8)
385
398
(set-buffer-process-coding-system 'utf-8 'utf-8)
386
(rename-buffer agda2-bufname)))
387
(apply 'agda2-go nil ":set" agda2-ghci-options)
388
(agda2-go nil ":mod +" agda2-toplevel-module)
399
(rename-buffer agda2-bufname)
400
(set-process-query-on-exit-flag agda2-process nil)))
401
(apply 'agda2-call-ghci ":set" agda2-ghci-options)
402
(agda2-call-ghci ":mod +" agda2-toplevel-module)
403
(agda2-remove-annotations))
391
405
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
392
406
;;;; Communicating with Agda
406
420
(comint-send-string proc chunk)))
407
421
(comint-send-string proc "\n"))
409
(defun agda2-go (require-response &rest args)
423
(defun agda2-call-ghci (&rest args)
410
424
"Executes commands in GHCi.
411
425
Sends the list of strings ARGS to GHCi, waits for output and
412
executes the responses, if any. If REQUIRE-RESPONSE is non-nil
413
then an error is raised if no responses are received."
426
executes the responses, if any. Returns the number of processed
415
428
(unless (eq 'run (agda2-process-status))
416
429
;; Try restarting automatically, but only once, in case there is
417
430
;; some major problem.
419
432
(unless (eq 'run (agda2-process-status))
420
433
(agda2-raise-ghci-error)))
422
(haskell-ghci-go (apply 'concat (agda2-intersperse " " args)) nil))
435
;; By setting local-enable-local-variables to nil the call to
436
;; hack-local-variables in haskell-ghci-go becomes more or less a
437
;; no-op. (Note that hack-local-variables can interfere with the
438
;; setup of a mode, because it can potentially perform the setup
439
;; of another mode...)
440
(let ((local-enable-local-variables nil))
441
(haskell-ghci-go (apply 'concat (agda2-intersperse " " args))
424
444
(with-current-buffer haskell-ghci-process-buffer
425
445
(haskell-ghci-wait-for-output)
433
453
(setq response (buffer-substring-no-properties
434
454
(point-min) (point-max)))))
435
455
(delete-file tempfile))))
436
(when (and (>= 0 (agda2-respond response))
438
(agda2-raise-ghci-error))))
440
(defun agda2-goal-cmd (require-response cmd &optional want ask &rest args)
441
"When in a goal, send CMD, goal num and range, and strings ARGS to agda2.
442
WANT is an optional prompt. When ASK is non-nil, use minibuffer.
443
If REQUIRE-RESPONSE is non-nil then an error is raised if no
444
responses are received."
456
(agda2-respond response)))
458
(defun agda2-go (highlight require-response update-goals &rest args)
459
"Executes commands in GHCi.
460
Sends the list of strings ARGS to GHCi, waits for output and
461
executes the responses, if any. An error is raised if no
462
responses are received (unless REQUIRE-RESPONSE is nil), and
463
otherwise the syntax highlighting information is reloaded (unless
464
HIGHLIGHT is nil; if HIGHLIGHT is a string, then highlighting
465
info is read from the corresponding file) and the goals
466
updated (unless UPDATE-GOALS is nil)."
467
(let* ((highlighting-temp (and highlight (not (stringp highlight))))
468
(highlighting (cond ((stringp highlight) highlight)
469
(highlighting-temp (make-temp-file "agda2-mode")))))
472
(apply 'agda2-call-ghci
474
(agda2-string-quote (buffer-file-name))
475
(if highlighting-temp
477
(agda2-string-quote highlighting)
481
(append args '(")")))))
482
(when (and require-response (>= 0 no-responses))
483
(agda2-raise-ghci-error))
484
(if highlight (agda2-highlight-load highlighting)))
485
(if highlighting-temp (delete-file highlighting))))
486
(if update-goals (agda2-annotate)))
488
(defun agda2-goal-cmd (cmd &optional want ask &rest args)
489
"Reads input from goal or minibuffer and sends command to Agda.
491
An error is raised if point is not in a goal.
493
The command sent to Agda is
495
CMD <goal number> <goal range> <user input> ARGS.
497
The user input is computed as follows:
499
* If WANT is nil, then the user input is the empty string.
501
* If WANT is a string, and either ASK is non-nil or the goal only
502
contains whitespace, then the input is taken from the
503
minibuffer. In this case WANT is used as the prompt string.
505
* Otherwise (including if WANT is 'goal) the goal contents is
508
An error is raised if no responses are received."
445
509
(multiple-value-bind (o g) (agda2-goal-at (point))
446
510
(unless g (error "For this command, please place the cursor in a goal"))
447
511
(let ((txt (buffer-substring-no-properties (+ (overlay-start o) 2)
448
512
(- (overlay-end o) 2))))
449
(if (not want) (setq txt "")
450
(when (or ask (string-match "\\`\\s *\\'" txt))
451
(setq txt (read-string (concat want ": ") txt))))
452
(apply 'agda2-go require-response cmd
513
(cond ((null want) (setq txt ""))
515
(or ask (string-match "\\`\\s *\\'" txt)))
516
(setq txt (read-string (concat want ": ") txt))))
517
(apply 'agda2-go nil t t cmd
454
519
(agda2-goal-Range o)
455
520
(agda2-string-quote txt) args))))
472
537
(eval (read response))))
540
(defvar agda2-response nil
541
"Used by the backend to give responses to the Agda mode.")
542
(make-variable-buffer-local 'agda2-response)
544
(defun agda2-ask (&rest args)
545
"Executes a query in GHCi and returns the response string."
546
(setq agda2-response 'agda2-no-response)
547
(apply 'agda2-go nil nil nil args)
548
(if (equal agda2-response 'agda2-no-response)
549
(agda2-raise-ghci-error)
475
552
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
476
553
;;;; User commands and response processing
478
555
(defun agda2-load ()
479
556
"Load current buffer."
481
(agda2-go t "cmd_load"
558
(agda2-go t t t "cmd_load"
482
559
(agda2-string-quote (buffer-file-name))
483
560
(agda2-list-quote agda2-include-dirs)
486
563
(defun agda2-compile ()
487
564
"Compile the current module."
489
(agda2-go t "cmd_compile"
566
(agda2-go t t t "cmd_compile"
490
567
(agda2-string-quote (buffer-file-name))
491
568
(agda2-list-quote agda2-include-dirs)
494
(defun agda2-load-action (gs)
495
"Annotate new goals GS in current buffer."
498
571
(defun agda2-give()
499
572
"Give to the goal at point the expression in it" (interactive)
500
(agda2-goal-cmd t "cmd_give" "expression to give"))
573
(agda2-goal-cmd "cmd_give" "expression to give"))
502
575
(defun agda2-give-action (old-g paren)
503
576
"Update the goal OLD-G with the expression in it."
504
577
(agda2-update old-g paren))
506
579
(defun agda2-refine ()
507
"Refine the goal at point by the expression in it." (interactive)
508
(agda2-goal-cmd t "cmd_refine" "expression to refine"))
580
"Refine the goal at point.
581
If the goal contains an expression e, and some \"suffix\" of the
582
type of e unifies with the goal type, then the goal is replaced
583
by e applied to a suitable number of new goals.
585
If the goal is empty, the goal type is a data type, and there is
586
exactly one constructor which unifies with this type, then the
587
goal is replaced by the constructor applied to a suitable number
590
(agda2-goal-cmd "cmd_refine_or_intro" 'goal))
593
"Simple proof search" (interactive)
594
(agda2-goal-cmd "cmd_auto"))
510
596
(defun agda2-make-case ()
511
597
"Refine the pattern var given in the goal.
512
598
Assumes that <clause> = {!<var>!} is on one line."
514
(agda2-goal-cmd t "cmd_make_case" "partten var to case"))
600
(agda2-goal-cmd "cmd_make_case" "pattern var to case"))
516
602
(defun agda2-make-case-action (newcls)
517
603
"Replace the line at point with new clauses NEWCLS and reload."
557
643
(defun agda2-show-goals()
558
644
"Show all goals." (interactive)
559
(agda2-go t "cmd_metas"))
645
(agda2-go t t t "cmd_metas"))
561
647
(defun agda2-show-constraints()
562
648
"Show constraints." (interactive)
563
(agda2-go t "cmd_constraints"))
649
(agda2-go t t t "cmd_constraints"))
565
(defun agda2-text-state ()
566
"UNDER CONSTRUCTION" (interactive)
651
(defun agda2-remove-annotations ()
652
"Removes buffer annotations (overlays and text properties)."
567
654
(dolist (o (overlays-in (point-min) (point-max)))
568
655
(delete-overlay o))
569
(agda2-go nil "cmd_reset")
570
656
(let ((inhibit-read-only t))
571
657
(annotation-preserve-mod-p-and-undo
572
658
(set-text-properties (point-min) (point-max) '()))
584
670
(or (go (point)) (go wrapped) (message "No goals in the buffer"))))
586
672
(defun agda2-quit ()
587
"Quit and clean up after agda2." (interactive)
673
"Quit and clean up after agda2."
588
675
(agda2-protect (progn (kill-buffer agda2-buffer)
589
676
(kill-buffer (current-buffer)))))
591
(defmacro agda2-maybe-normalised (name comment cmd prompt)
678
(defmacro agda2-maybe-normalised (name comment cmd want)
592
679
"This macro constructs a function NAME which runs CMD.
593
680
COMMENT is used to build the function's comment. The function
594
681
NAME takes a prefix argument which tells whether it should
595
682
normalise types or not when running CMD (through
596
`agda2-goal-cmd' t; PROMPT, if non-nil, is used as the goal
683
`agda2-goal-cmd'; WANT is used as `agda2-goal-cmd's WANT
598
685
(let ((eval (make-symbol "eval")))
599
686
`(defun ,name (&optional not-normalise)
600
687
,(concat comment ".
602
689
With a prefix argument the result is not explicitly normalised.")
603
690
(interactive "P")
604
691
(let ((,eval (if not-normalise "Instantiated" "Normalised")))
605
(agda2-goal-cmd t (concat ,cmd " Agda.Interaction.BasicOps." ,eval)
692
(agda2-goal-cmd (concat ,cmd " Agda.Interaction.BasicOps." ,eval)
608
695
(defmacro agda2-maybe-normalised-toplevel (name comment cmd prompt)
609
696
"This macro constructs a function NAME which runs CMD.
610
697
COMMENT is used to build the function's comments. The function
611
698
NAME takes a prefix argument which tells whether it should
612
normalise types or not when running CMD (through `agda2-go' t; the
613
string PROMPT is used as the goal command prompt)."
699
normalise types or not when running CMD (through
700
`agda2-go' nil t nil; the string PROMPT is used as the goal
614
702
(let ((eval (make-symbol "eval")))
615
703
`(defun ,name (not-normalise expr)
616
704
,(concat comment ".
618
706
With a prefix argument the result is not explicitly normalised.")
619
707
(interactive ,(concat "P\nM" prompt ": "))
620
708
(let ((,eval (if not-normalise "Instantiated" "Normalised")))
621
(agda2-go t (concat ,cmd " Agda.Interaction.BasicOps." ,eval " "
622
(agda2-string-quote expr)))))))
710
(concat ,cmd " Agda.Interaction.BasicOps." ,eval " "
711
(agda2-string-quote expr)))))))
624
713
(agda2-maybe-normalised
713
802
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
716
(defun agda2-annotate (goals)
805
(defun agda2-highlight-reload nil
806
"Loads precomputed syntax highlighting info for the current buffer.
807
If there is any to load."
808
(let ((highlighting (make-temp-file "agda2-mode")))
811
(agda2-go highlighting nil t
812
"cmd_write_highlighting_info"
813
(agda2-string-quote (buffer-file-name))
814
(agda2-string-quote highlighting)))
815
(delete-file highlighting))))
817
(defun agda2-annotate ()
717
818
"Annotates the goals in the current buffer with text properties.
718
The goal numbers should be given by GOALS (in the order they
719
appear in the buffer)."
819
Note that this function should be run /after/ syntax highlighting
820
information has been loaded, because the two highlighting
821
mechanisms interact in unfortunate ways."
720
822
(agda2-forget-all-goals)
826
(goals (agda2-ask "cmd_goals"
827
(agda2-string-quote (buffer-file-name)))))
722
828
((delims() (re-search-forward "[?]\\|[{][-!]\\|[-!][}]\\|--" nil t))
723
829
(is-lone-questionmark ()
814
920
(let(ys)(while xs (push (pop xs) ys)(push sep ys))(pop ys)(nreverse ys)))
816
922
(defun agda2-goal-Range (o)
817
"Range of goal overlay O."
923
"The Haskell Range of goal overlay O."
818
924
(format "(Range [Interval %s %s])"
819
925
(agda2-mkPos (+ (overlay-start o) 2))
820
926
(agda2-mkPos (- (overlay-end o) 2))))
822
928
(defun agda2-mkPos (&optional p)
823
"Position value of P or point."
929
"The Haskell Position corresponding to P or `point'."
825
931
(if p (goto-char p))
826
(format "(Pn \"%s\" %d %d %d)" (buffer-file-name)
827
(point) (count-lines (point-min) (point)) (1+ (current-column)))))
932
(format "(Pn (Just (mkAbsolute %s)) %d %d %d)"
933
(agda2-string-quote (file-truename (buffer-file-name)))
935
(count-lines (point-min) (point))
936
(1+ (current-column)))))
829
938
(defun agda2-char-quote (c)
830
939
"Convert character C to the notation used in Haskell strings.
1022
1131
With prefix argument, turn on display of implicit arguments if
1023
1132
the argument is a positive number, otherwise turn it off."
1024
1133
(interactive "P")
1025
(cond ((eq arg nil) (agda2-go t "toggleImplicitArgs"))
1134
(cond ((eq arg nil) (agda2-go t t t "toggleImplicitArgs"))
1026
1135
((and (numberp arg)
1027
(> arg 0)) (agda2-go t "showImplicitArgs" "True"))
1028
(t (agda2-go t "showImplicitArgs" "False"))))
1136
(> arg 0)) (agda2-go t t t "showImplicitArgs" "True"))
1137
(t (agda2-go t t t "showImplicitArgs" "False"))))
1030
1139
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
added
removed
src/data/emacs-mode/agda2-mode.el
