Initial ligation support for Dafny (#1271)

This commit is contained in:
be5invis 2022-01-04 20:12:19 -08:00
parent 68d054448a
commit 067e06b3e1
2 changed files with 16 additions and 2 deletions

View file

@ -43,8 +43,12 @@ define [buildLigationsImpl sink para featureName mappedFeature rankedLookups] :
define underscore {'underscore'}
define regexLookAround [less.concat hyphen equal exclam greater anyBar]
define [acops] {'less' 'greater' 'hyphen' 'equal' 'plus'}
define [acskip] {'slash' 'bar' 'at' 'ampersand' 'percent' 'numberSign'}
define [acops] : if [hasLG 'bar-triggers-op-centering']
begin {'less' 'greater' 'hyphen' 'equal' 'plus' 'slash' 'bar' 'backslash'}
begin {'less' 'greater' 'hyphen' 'equal' 'plus'}
define [acskip] : if [hasLG 'bar-triggers-op-centering']
begin {'at' 'ampersand' 'percent' 'numberSign'}
begin {'slash' 'bar' 'backslash' 'at' 'ampersand' 'percent' 'numberSign'}
local ligationLookupName : 'lig_' + featureName + '{' + mappedFeature + '}'

View file

@ -147,6 +147,11 @@ ligGroup = "dot-oper"
samples = ["<.", "<.>", ".>"]
desc = 'Treat dot (`.`) as operator and perform chained centering'
[simple.bar-triggers-op-centering]
ligGroup = "bar-triggers-op-centering"
samples = [":|", ":|:", "|:"]
desc = 'Bars (`/`, `|`, `\`) will trigger operator centering'
[simple.lteq-as-arrow]
ligGroup = "arrowZALE"
samples = ["<="]
@ -277,6 +282,11 @@ tag = 'SWFT'
buildup = ['center-ops', 'arrow', 'arrow2', 'trig', 'llgg', 'eqeq', 'exeq', 'ineq', 'ltgt-diamond', 'plusplus', 'kern-dotty', 'kern-bars']
desc = 'Swift'
[composite.dafny]
tag = 'DFNY'
buildup = ['center-ops', 'arrow', 'arrow2', 'trig', 'llgg', 'eqeq', 'exeq', 'ineq', 'ltgt-diamond', 'plusplus', 'bar-triggers-op-centering', 'kern-dotty', 'kern-bars']
desc = 'Dafny'
[composite.coq]
tag = 'COQX'
buildup = ['center-ops', 'arrow', 'arrow2', 'trig', 'llgg', 'eqeq', 'ltgt-ne', 'ineq', 'plusplus', 'dot-as-operator', 'logic', 'brst', 'kern-dotty', 'kern-bars']