feat: expose optionValue parser (#10839)

leodemoura · web-flow · commit 61ee3b271102 · 2025-10-19T22:57:47.000Z
This PR exposes the `optionValue` parser used to implement the
`set_option` notation.
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
@@ -909,14 +909,15 @@ abbrev declModifiersT := declModifiers true
 builtin_initialize
   register_parser_alias (kind := ``declModifiers) "declModifiers"       declModifiersF
   register_parser_alias (kind := ``declModifiers) "nestedDeclModifiers" declModifiersT
-  register_parser_alias                                                 declId
-  register_parser_alias                                                 declSig
-  register_parser_alias                                                 declVal
-  register_parser_alias                                                 optDeclSig
-  register_parser_alias                                                 openDecl
-  register_parser_alias                                                 docComment
-  register_parser_alias                                                 plainDocComment
-  register_parser_alias                                                 visibility
+  register_parser_alias declId
+  register_parser_alias declSig
+  register_parser_alias declVal
+  register_parser_alias optDeclSig
+  register_parser_alias openDecl
+  register_parser_alias docComment
+  register_parser_alias plainDocComment
+  register_parser_alias visibility
+  register_parser_alias "optionValue" Command.optionValue
 
 /--
 Registers an error explanation.
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+// update me!`
`1`	`2`	`#include "util/options.h"`
`2`	`3`
`3`	`4`	`namespace lean {`