> You have something like that in Coq/ex/indent.v.
> I dream of a smie with two grammars (and lexers): one for first lines of
> commands and one inside commands. It would greatly simplify things I think.
I don't really know how to define "first lines" and "inside", but you
can definitely have "two grammars" with SMIE:
You can combine two smie-grammars with something like
(append (mapcar (lambda (x) (cons (concat "1" (car x)) (cdr x)))
grammar1)
(mapcar (lambda (x) (cons (concat "2" (car x)) (cdr x)))
grammar2))
then you can combine the two tokenizing functions with:
(defun combined-fun ()
(if (in-first-lines-of-commands)
(let ((tok (fun1)))
(if tok (concat "1" tok)))
(let ((tok (fun2)))
(if tok (concat "2" tok)))))
this won't quite work right because:
- the tokenizer can return nil for open/close parens and such in which
case the above will fail to add the corresponding "1" or "2" prefix.
- the relative precedence of the two grammars is left unspecified so it
can lead to surprises when crossing between one part and the other.
But neither of those two problems are hard to fix, I think.
Stefan
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
