[vim/vim] runtime/syntax/sml.vim - wrongly red-colored brace (#5173)

15 views
Skip to first unread message

Anton Kochkov

unread,
Nov 4, 2019, 3:55:00 AM11/4/19
to vim/vim, Subscribed

Instructions: Replace the template text and remove irrelevant text (including this line)

Describe the bug
A clear and concise description of what the bug is.
(Issues related to the runtime files should be reported to their maintainer, check the file header.)

To Reproduce

  1. vim
  2. set ft=sml
  3. paste the following lines:
Definition eval_const_def:

  (eval_const g (IntC W1 i) = FlatV (W1V (i2w i))) ∧

  (eval_const g (IntC W8 i) = FlatV (W8V (i2w i))) ∧

  (eval_const g (IntC W32 i) = FlatV (W32V (i2w i))) ∧

  (eval_const g (IntC W64 i) = FlatV (W64V (i2w i))) ∧

  (eval_const g (StrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧

  (eval_const g (ArrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧

  (eval_const g (GepC ty ptr (t, idx) indices) =

    case (eval_const g ptr, signed_v_to_num (eval_const g idx)) of

    | (FlatV (PtrV ptr), Some n) =>

      let ns = map (λ(t,ci). case signed_v_to_num (eval_const g ci) of None => 0 | Some n => n) indices in

        (case get_offset ty ns of

         | None => FlatV UndefV

         | Some off => FlatV (PtrV (n2w ((w2n ptr) + (sizeof ty) * n + off))))

    | _ => FlatV UndefV) ∧

  (eval_const g (GlobalC var) =

    case flookup g var of

    | None => FlatV (PtrV 0w)

    | Some (s,w) => FlatV (PtrV w)) ∧

  (eval_const g UndefC = FlatV UndefV)

Termination

  WF_REL_TAC `measure (const_size o snd)` >> rw [listTheory.MEM_MAP] >>

  TRY

    (TRY (PairCases_on `y`) >> simp [] >>

    Induct_on `tconsts` >> rw [] >> rw [definition "const_size_def"] >>

    res_tac >> fs [] >> NO_TAC) >>

  Induct_on `indices` >> rw [] >> rw [definition "const_size_def"] >>

  fs []

End

One more case are these lines:

open HolKernel boolLib bossLib Parse;

open llistTheory pathTheory;

open settingsTheory memory_modelTheory;



new_theory "llvm";



numLib.prefer_num ();

Expected behavior

Do not highlight these braces with red color.

Screenshots

image

Environment (please complete the following information):

  • Vim version 8.1.2198
  • OS: Fedora 31
  • Terminal: Konsole

Additional context

The original file with this source code is from https://github.com/facebook/infer/blob/master/sledge/semantics/llvmScript.sml

cc @mmottl

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or unsubscribe.

Christian Brabandt

unread,
Nov 4, 2019, 4:03:05 AM11/4/19
to vim/vim, Subscribed

have you contacted the maintainer of the file?

Anton Kochkov

unread,
Nov 4, 2019, 4:04:49 AM11/4/19
to vim/vim, Subscribed

Yes, I put him in cc of this issue.

Christian Brabandt

unread,
Nov 4, 2019, 4:07:46 AM11/4/19
to vim/vim, Subscribed

well, it's a bit strange to open the issue here, when there is a specific method to contact the maintainer. Oh well.

Markus Mottl

unread,
Nov 7, 2019, 6:35:07 PM11/7/19
to vim/vim, Subscribed

I don't actively maintain the SML Vim file anymore. Though you can submit a PR at https://github.com/mmottl/vim-files, I don't usually sync my Vim files upstream anymore. I guess the fastest way to get anything fixed upstream would be to open a PR right here (please correct me if there is a better way).

Doug Kearns

unread,
Nov 17, 2021, 7:14:19 AM11/17/21
to vim/vim, Subscribed

That's some sort of HOL variant not SML.

—
You are receiving this because you are subscribed to this thread.

Reply to this email directly, view it on GitHub.
Triage notifications on the go with GitHub Mobile for iOS or Android.

dkearns

unread,
Mar 25, 2026, 3:26:50 AM (yesterday) Mar 25
to vim/vim, Subscribed

Closed #5173 as completed.

—


Reply to this email directly, view it on GitHub, or unsubscribe.

You are receiving this because you are subscribed to this thread.Message ID: <vim/vim/issue/5173/issue_event/23879711330@github.com>

Reply all
Reply to author
Forward
0 new messages