diff --git a/stage0/src/Lean/Parser/Basic.lean b/stage0/src/Lean/Parser/Basic.lean
index e04d58825e..4b1d7c3a3d 100644
--- a/stage0/src/Lean/Parser/Basic.lean
+++ b/stage0/src/Lean/Parser/Basic.lean
@@ -120,9 +120,10 @@ instance InputContext.inhabited : Inhabited InputContext :=
 ⟨{ input := "", fileName := "", fileMap := arbitrary _ }⟩
 
 structure ParserContext extends InputContext :=
-(prec     : Nat)
-(env      : Environment)
-(tokens   : TokenTable)
+(prec       : Nat)
+(env        : Environment)
+(tokens     : TokenTable)
+(insideQuot : Bool := false)
 
 structure Error :=
 (unexpected : String := "")
@@ -360,6 +361,31 @@ fun c s =>
 { info := epsilonInfo,
   fn   := checkPrecFn prec }
 
+def checkInsideQuotFn : ParserFn :=
+fun c s =>
+  if c.insideQuot then s
+  else s.mkUnexpectedError "unexpected syntax outside syntax quotation"
+
+@[inline] def checkInsideQuot : Parser :=
+{ info := epsilonInfo,
+  fn   := checkInsideQuotFn }
+
+def checkOutsideQuotFn : ParserFn :=
+fun c s =>
+  if !c.insideQuot then s
+  else s.mkUnexpectedError "unexpected syntax inside syntax quotation"
+
+@[inline] def checkOutsideQuot : Parser :=
+{ info := epsilonInfo,
+  fn   := checkOutsideQuotFn }
+
+def toggleInsideQuotFn (p : ParserFn) : ParserFn :=
+fun c s => p { c with insideQuot := !c.insideQuot } s
+
+@[inline] def toggleInsideQuot (p : Parser) : Parser :=
+{ info := epsilonInfo,
+  fn   := toggleInsideQuotFn p.fn }
+
 @[inline] def leadingNode (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser :=
 checkPrec prec >> node n p
 
diff --git a/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean b/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean
index 02feef5345..9c1089543b 100644
--- a/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -406,12 +406,18 @@ p ⟨0, 0⟩
 def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer :=
 p
 
+@[combinatorParenthesizer Lean.Parser.toggleInsideQuot]
+def toggleInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer :=
+p
+
 @[combinatorParenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkTailWs] def checkTailWs.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkColGe] def checkColGe.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer := pure ()
+@[combinatorParenthesizer Lean.Parser.checkInsideQuot] def checkInsideQuot.parenthesizer : Parenthesizer := pure ()
+@[combinatorParenthesizer Lean.Parser.checkOutsideQuot] def checkOutsideQuot.parenthesizer : Parenthesizer := pure ()
 
 @[combinatorParenthesizer Lean.Parser.pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft
 
diff --git a/stage0/stdlib/Lean/Elab/Quotation.c b/stage0/stdlib/Lean/Elab/Quotation.c
index 9cb734303d..831608ef0d 100644
--- a/stage0/stdlib/Lean/Elab/Quotation.c
+++ b/stage0/stdlib/Lean/Elab/Quotation.c
@@ -26185,7 +26185,7 @@ return x_1;
 lean_object* lean_parse_expr(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
 x_4 = l_Lean_Elab_Term_Quotation_oldParseExpr___closed__1;
 lean_inc(x_2);
 x_5 = l_Lean_Parser_mkInputContext(x_2, x_4);
@@ -26194,43 +26194,45 @@ lean_dec(x_2);
 x_7 = l_Lean_Parser_ParserState_setPos(x_6, x_3);
 x_8 = l_Lean_Parser_getTokenTable(x_1);
 x_9 = l_Lean_Parser_maxPrec;
-x_10 = lean_alloc_ctor(0, 4, 0);
-lean_ctor_set(x_10, 0, x_5);
-lean_ctor_set(x_10, 1, x_9);
-lean_ctor_set(x_10, 2, x_1);
-lean_ctor_set(x_10, 3, x_8);
-x_11 = l_Lean_Parser_termParser___closed__2;
-x_12 = l_Lean_Parser_categoryParser___elambda__1(x_11, x_9, x_10, x_7);
-x_13 = lean_ctor_get(x_12, 3);
-lean_inc(x_13);
-if (lean_obj_tag(x_13) == 0)
-{
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
-x_14 = lean_ctor_get(x_12, 0);
+x_10 = 0;
+x_11 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_11, 0, x_5);
+lean_ctor_set(x_11, 1, x_9);
+lean_ctor_set(x_11, 2, x_1);
+lean_ctor_set(x_11, 3, x_8);
+lean_ctor_set_uint8(x_11, sizeof(void*)*4, x_10);
+x_12 = l_Lean_Parser_termParser___closed__2;
+x_13 = l_Lean_Parser_categoryParser___elambda__1(x_12, x_9, x_11, x_7);
+x_14 = lean_ctor_get(x_13, 3);
 lean_inc(x_14);
-x_15 = lean_ctor_get(x_12, 1);
+if (lean_obj_tag(x_14) == 0)
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_15 = lean_ctor_get(x_13, 0);
 lean_inc(x_15);
-lean_dec(x_12);
-x_16 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_14);
-lean_dec(x_14);
-x_17 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_17, 0, x_16);
-lean_ctor_set(x_17, 1, x_15);
-x_18 = lean_alloc_ctor(1, 1, 0);
+x_16 = lean_ctor_get(x_13, 1);
+lean_inc(x_16);
+lean_dec(x_13);
+x_17 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_15);
+lean_dec(x_15);
+x_18 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_18, 0, x_17);
-return x_18;
+lean_ctor_set(x_18, 1, x_16);
+x_19 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_19, 0, x_18);
+return x_19;
 }
 else
 {
-lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-lean_dec(x_12);
-x_19 = lean_ctor_get(x_13, 0);
-lean_inc(x_19);
+lean_object* x_20; lean_object* x_21; lean_object* x_22; 
 lean_dec(x_13);
-x_20 = l_Lean_Parser_Error_toString(x_19);
-x_21 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_21, 0, x_20);
-return x_21;
+x_20 = lean_ctor_get(x_14, 0);
+lean_inc(x_20);
+lean_dec(x_14);
+x_21 = l_Lean_Parser_Error_toString(x_20);
+x_22 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_22, 0, x_21);
+return x_22;
 }
 }
 }
diff --git a/stage0/stdlib/Lean/Parser/Basic.c b/stage0/stdlib/Lean/Parser/Basic.c
index b4c993df6f..9bf049bf3a 100644
--- a/stage0/stdlib/Lean/Parser/Basic.c
+++ b/stage0/stdlib/Lean/Parser/Basic.c
@@ -71,6 +71,7 @@ lean_object* l_Lean_Parser_optionaInfo___elambda__2(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_ParserFn_inhabited___rarg(lean_object*);
 lean_object* l_Lean_Parser_binNumberFn___closed__1;
 lean_object* l_Lean_Parser_hexNumberFn___closed__1;
+lean_object* l_Lean_Parser_checkInsideQuotFn(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_foldSepRevArgs(lean_object*);
 lean_object* l_Lean_Parser_binNumberFn___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_numberFnAux(lean_object*, lean_object*);
@@ -270,6 +271,7 @@ lean_object* l_Lean_Parser_takeWhileFn(lean_object*, lean_object*, lean_object*)
 lean_object* l_Lean_Parser_numLit___closed__2;
 lean_object* l_Array_foldlStepMAux___main___at_Lean_Syntax_foldSepArgsM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_nonReservedSymbolInfo___elambda__2(lean_object*);
+lean_object* l_Lean_Parser_checkOutsideQuot___closed__1;
 lean_object* l_Lean_Parser_initCacheForInput(lean_object*);
 lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_identFnAux___main___spec__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__4;
@@ -398,6 +400,7 @@ lean_object* l_Lean_Parser_Error_HasBeq;
 lean_object* l_Lean_Parser_nonReservedSymbolInfo___closed__3;
 lean_object* l_Lean_Parser_Error_Inhabited___closed__1;
 lean_object* l_Lean_Parser_ParserState_shrinkStack(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_checkOutsideQuot___closed__2;
 uint8_t l_Lean_Parser_checkTailNoWs(lean_object*);
 lean_object* l_Lean_Parser_checkTailWs___boxed(lean_object*);
 lean_object* l_Lean_Parser_charLitFn(lean_object*, lean_object*);
@@ -493,6 +496,7 @@ lean_object* l_Lean_Parser_checkTailNoWs___boxed(lean_object*);
 lean_object* l_Lean_Parser_takeUntilFn(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_symbolNoWsInfo(lean_object*);
 lean_object* l_Lean_Parser_epsilonInfo___elambda__1___boxed(lean_object*);
+lean_object* l_Lean_Parser_checkOutsideQuot;
 lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_mkAtomicInfo___elambda__1(lean_object*);
 lean_object* l_Lean_Parser_anyOfFn(lean_object*, lean_object*, lean_object*);
@@ -500,11 +504,13 @@ lean_object* l_Lean_Parser_mkEmptySubstringAt(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_takeWhileFn___at_Lean_Parser_binNumberFn___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_strLitFnAux___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Error_toString___closed__2;
+lean_object* l_Lean_Parser_checkInsideQuot;
 lean_object* l_Lean_Parser_nameLitNoAntiquot___closed__3;
 lean_object* l_Array_foldlStepMAux___main___at_Lean_Syntax_foldSepArgs___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_Prim_Ref_get___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_longestMatchMkResult(lean_object*, lean_object*);
 size_t l_USize_mul(size_t, size_t);
+lean_object* l_Lean_Parser_toggleInsideQuot(lean_object*);
 lean_object* l_Lean_Parser_whitespace(lean_object*, lean_object*);
 lean_object* l_List_redLength___main___rarg(lean_object*);
 lean_object* l_Lean_Parser_rawCh(uint32_t, uint8_t);
@@ -523,6 +529,7 @@ lean_object* l_Lean_Parser_termParser(lean_object*);
 lean_object* l_Lean_Parser_sepByFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_FirstTokens_toStr___closed__3;
 lean_object* l_Lean_Parser_manyAux(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_checkInsideQuotFn___closed__1;
 lean_object* l_Lean_Parser_mkAntiquot___closed__7;
 uint8_t l_List_beq___main___at_Lean_Syntax_structEq___main___spec__3(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_pushNone___closed__1;
@@ -541,8 +548,10 @@ lean_object* l_Lean_Parser_rawIdentNoAntiquot___closed__2;
 size_t l_USize_land(size_t, size_t);
 lean_object* l_Lean_Parser_nameLit___elambda__1___closed__1;
 lean_object* l_Lean_Parser_mkAntiquot___elambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_checkOutsideQuotFn(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_foldlStepMAux___main___at_Array_foldSepByM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_checkInsideQuot___closed__1;
 extern lean_object* l___private_Lean_Environment_5__envExtensionsRef;
 lean_object* l_Lean_Parser_mkCategoryParserFnExtension___closed__1;
 lean_object* l_Lean_Parser_sepBy1Info(lean_object*, lean_object*);
@@ -550,12 +559,14 @@ lean_object* l_Lean_Parser_quotedCharFn___closed__1;
 lean_object* l_Lean_Parser_charLitFnAux___closed__1;
 lean_object* l_Lean_Parser_symbolNoWs(lean_object*);
 lean_object* l_Lean_Parser_hexDigitFn___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_checkInsideQuotFn___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_ParserState_mergeErrors___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_foldSepBy(lean_object*);
 lean_object* l_Lean_Parser_categoryParserFnExtension___elambda__2(lean_object*);
 lean_object* l_Lean_Parser_trailingNode(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_orelseInfo___elambda__2(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_checkInsideQuot___closed__2;
 lean_object* l_Lean_Parser_pushNone___closed__2;
 lean_object* l_Lean_Parser_quotedCharFn___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_sepBy1(lean_object*, lean_object*, uint8_t, uint8_t);
@@ -581,6 +592,7 @@ lean_object* l_Lean_Parser_symbol___boxed(lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_foldArgs___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_charLit___elambda__1(lean_object*, lean_object*);
 uint8_t l_UInt32_decEq(uint32_t, uint32_t);
+lean_object* l_Lean_Parser_toggleInsideQuotFn(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Syntax_inhabited;
 lean_object* l_Lean_Parser_unquotedSymbolFn(lean_object*, lean_object*);
 lean_object* l_String_intercalate(lean_object*, lean_object*);
@@ -723,7 +735,9 @@ lean_object* l_Array_toList___rarg(lean_object*);
 lean_object* l_Lean_Parser_checkWsBeforeFn___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_optionalFn(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_nameLitFn___closed__1;
+lean_object* l_Lean_Parser_checkOutsideQuotFn___closed__1;
 lean_object* l_Std_PersistentHashMap_insertAux___main___at_Lean_Parser_SyntaxNodeKindSet_insert___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_checkOutsideQuotFn___boxed(lean_object*, lean_object*);
 lean_object* lean_array_pop(lean_object*);
 lean_object* l_Lean_Parser_TokenMap_insert___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_isIdFirst(uint32_t);
@@ -3969,6 +3983,225 @@ lean_ctor_set(x_4, 1, x_2);
 return x_4;
 }
 }
+lean_object* _init_l_Lean_Parser_checkInsideQuotFn___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("unexpected syntax outside syntax quotation");
+return x_1;
+}
+}
+lean_object* l_Lean_Parser_checkInsideQuotFn(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; 
+x_3 = lean_ctor_get_uint8(x_1, sizeof(void*)*4);
+if (x_3 == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+x_4 = l_Lean_Parser_checkInsideQuotFn___closed__1;
+x_5 = l_Lean_Parser_ParserState_mkUnexpectedError(x_2, x_4);
+return x_5;
+}
+else
+{
+return x_2;
+}
+}
+}
+lean_object* l_Lean_Parser_checkInsideQuotFn___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Parser_checkInsideQuotFn(x_1, x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_checkInsideQuot___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Parser_checkInsideQuotFn___boxed), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Parser_checkInsideQuot___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_epsilonInfo;
+x_2 = l_Lean_Parser_checkInsideQuot___closed__1;
+x_3 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_3, 0, x_1);
+lean_ctor_set(x_3, 1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_checkInsideQuot() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_Parser_checkInsideQuot___closed__2;
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Parser_checkOutsideQuotFn___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("unexpected syntax inside syntax quotation");
+return x_1;
+}
+}
+lean_object* l_Lean_Parser_checkOutsideQuotFn(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; 
+x_3 = lean_ctor_get_uint8(x_1, sizeof(void*)*4);
+if (x_3 == 0)
+{
+return x_2;
+}
+else
+{
+lean_object* x_4; lean_object* x_5; 
+x_4 = l_Lean_Parser_checkOutsideQuotFn___closed__1;
+x_5 = l_Lean_Parser_ParserState_mkUnexpectedError(x_2, x_4);
+return x_5;
+}
+}
+}
+lean_object* l_Lean_Parser_checkOutsideQuotFn___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Parser_checkOutsideQuotFn(x_1, x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_checkOutsideQuot___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Parser_checkOutsideQuotFn___boxed), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Parser_checkOutsideQuot___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_epsilonInfo;
+x_2 = l_Lean_Parser_checkOutsideQuot___closed__1;
+x_3 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_3, 0, x_1);
+lean_ctor_set(x_3, 1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_checkOutsideQuot() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_Parser_checkOutsideQuot___closed__2;
+return x_1;
+}
+}
+lean_object* l_Lean_Parser_toggleInsideQuotFn(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+uint8_t x_4; 
+x_4 = lean_ctor_get_uint8(x_2, sizeof(void*)*4);
+if (x_4 == 0)
+{
+uint8_t x_5; 
+x_5 = !lean_is_exclusive(x_2);
+if (x_5 == 0)
+{
+uint8_t x_6; lean_object* x_7; 
+x_6 = 1;
+lean_ctor_set_uint8(x_2, sizeof(void*)*4, x_6);
+x_7 = lean_apply_2(x_1, x_2, x_3);
+return x_7;
+}
+else
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; lean_object* x_13; lean_object* x_14; 
+x_8 = lean_ctor_get(x_2, 0);
+x_9 = lean_ctor_get(x_2, 1);
+x_10 = lean_ctor_get(x_2, 2);
+x_11 = lean_ctor_get(x_2, 3);
+lean_inc(x_11);
+lean_inc(x_10);
+lean_inc(x_9);
+lean_inc(x_8);
+lean_dec(x_2);
+x_12 = 1;
+x_13 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_13, 0, x_8);
+lean_ctor_set(x_13, 1, x_9);
+lean_ctor_set(x_13, 2, x_10);
+lean_ctor_set(x_13, 3, x_11);
+lean_ctor_set_uint8(x_13, sizeof(void*)*4, x_12);
+x_14 = lean_apply_2(x_1, x_13, x_3);
+return x_14;
+}
+}
+else
+{
+uint8_t x_15; 
+x_15 = !lean_is_exclusive(x_2);
+if (x_15 == 0)
+{
+uint8_t x_16; lean_object* x_17; 
+x_16 = 0;
+lean_ctor_set_uint8(x_2, sizeof(void*)*4, x_16);
+x_17 = lean_apply_2(x_1, x_2, x_3);
+return x_17;
+}
+else
+{
+lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24; 
+x_18 = lean_ctor_get(x_2, 0);
+x_19 = lean_ctor_get(x_2, 1);
+x_20 = lean_ctor_get(x_2, 2);
+x_21 = lean_ctor_get(x_2, 3);
+lean_inc(x_21);
+lean_inc(x_20);
+lean_inc(x_19);
+lean_inc(x_18);
+lean_dec(x_2);
+x_22 = 0;
+x_23 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_23, 0, x_18);
+lean_ctor_set(x_23, 1, x_19);
+lean_ctor_set(x_23, 2, x_20);
+lean_ctor_set(x_23, 3, x_21);
+lean_ctor_set_uint8(x_23, sizeof(void*)*4, x_22);
+x_24 = lean_apply_2(x_1, x_23, x_3);
+return x_24;
+}
+}
+}
+}
+lean_object* l_Lean_Parser_toggleInsideQuot(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = lean_ctor_get(x_1, 1);
+lean_inc(x_2);
+lean_dec(x_1);
+x_3 = lean_alloc_closure((void*)(l_Lean_Parser_toggleInsideQuotFn), 3, 1);
+lean_closure_set(x_3, 0, x_2);
+x_4 = l_Lean_Parser_epsilonInfo;
+x_5 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_5, 0, x_4);
+lean_ctor_set(x_5, 1, x_3);
+return x_5;
+}
+}
 lean_object* l_Lean_Parser_leadingNode(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@@ -23569,21 +23802,23 @@ return x_7;
 }
 else
 {
-lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; 
 x_8 = lean_ctor_get(x_3, 0);
 x_9 = lean_ctor_get(x_3, 2);
 x_10 = lean_ctor_get(x_3, 3);
+x_11 = lean_ctor_get_uint8(x_3, sizeof(void*)*4);
 lean_inc(x_10);
 lean_inc(x_9);
 lean_inc(x_8);
 lean_dec(x_3);
-x_11 = lean_alloc_ctor(0, 4, 0);
-lean_ctor_set(x_11, 0, x_8);
-lean_ctor_set(x_11, 1, x_2);
-lean_ctor_set(x_11, 2, x_9);
-lean_ctor_set(x_11, 3, x_10);
-x_12 = l_Lean_Parser_categoryParserFn(x_1, x_11, x_4);
-return x_12;
+x_12 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_12, 0, x_8);
+lean_ctor_set(x_12, 1, x_2);
+lean_ctor_set(x_12, 2, x_9);
+lean_ctor_set(x_12, 3, x_10);
+lean_ctor_set_uint8(x_12, sizeof(void*)*4, x_11);
+x_13 = l_Lean_Parser_categoryParserFn(x_1, x_12, x_4);
+return x_13;
 }
 }
 }
@@ -26187,21 +26422,23 @@ return x_7;
 }
 else
 {
-lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; 
 x_8 = lean_ctor_get(x_3, 0);
 x_9 = lean_ctor_get(x_3, 2);
 x_10 = lean_ctor_get(x_3, 3);
+x_11 = lean_ctor_get_uint8(x_3, sizeof(void*)*4);
 lean_inc(x_10);
 lean_inc(x_9);
 lean_inc(x_8);
 lean_dec(x_3);
-x_11 = lean_alloc_ctor(0, 4, 0);
-lean_ctor_set(x_11, 0, x_8);
-lean_ctor_set(x_11, 1, x_2);
-lean_ctor_set(x_11, 2, x_9);
-lean_ctor_set(x_11, 3, x_10);
-x_12 = l_Lean_Parser_categoryParserOfStackFn(x_1, x_11, x_4);
-return x_12;
+x_12 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_12, 0, x_8);
+lean_ctor_set(x_12, 1, x_2);
+lean_ctor_set(x_12, 2, x_9);
+lean_ctor_set(x_12, 3, x_10);
+lean_ctor_set_uint8(x_12, sizeof(void*)*4, x_11);
+x_13 = l_Lean_Parser_categoryParserOfStackFn(x_1, x_12, x_4);
+return x_13;
 }
 }
 }
@@ -27778,6 +28015,22 @@ l_Lean_Parser_hasAndthen = _init_l_Lean_Parser_hasAndthen();
 lean_mark_persistent(l_Lean_Parser_hasAndthen);
 l_Lean_Parser_checkPrecFn___closed__1 = _init_l_Lean_Parser_checkPrecFn___closed__1();
 lean_mark_persistent(l_Lean_Parser_checkPrecFn___closed__1);
+l_Lean_Parser_checkInsideQuotFn___closed__1 = _init_l_Lean_Parser_checkInsideQuotFn___closed__1();
+lean_mark_persistent(l_Lean_Parser_checkInsideQuotFn___closed__1);
+l_Lean_Parser_checkInsideQuot___closed__1 = _init_l_Lean_Parser_checkInsideQuot___closed__1();
+lean_mark_persistent(l_Lean_Parser_checkInsideQuot___closed__1);
+l_Lean_Parser_checkInsideQuot___closed__2 = _init_l_Lean_Parser_checkInsideQuot___closed__2();
+lean_mark_persistent(l_Lean_Parser_checkInsideQuot___closed__2);
+l_Lean_Parser_checkInsideQuot = _init_l_Lean_Parser_checkInsideQuot();
+lean_mark_persistent(l_Lean_Parser_checkInsideQuot);
+l_Lean_Parser_checkOutsideQuotFn___closed__1 = _init_l_Lean_Parser_checkOutsideQuotFn___closed__1();
+lean_mark_persistent(l_Lean_Parser_checkOutsideQuotFn___closed__1);
+l_Lean_Parser_checkOutsideQuot___closed__1 = _init_l_Lean_Parser_checkOutsideQuot___closed__1();
+lean_mark_persistent(l_Lean_Parser_checkOutsideQuot___closed__1);
+l_Lean_Parser_checkOutsideQuot___closed__2 = _init_l_Lean_Parser_checkOutsideQuot___closed__2();
+lean_mark_persistent(l_Lean_Parser_checkOutsideQuot___closed__2);
+l_Lean_Parser_checkOutsideQuot = _init_l_Lean_Parser_checkOutsideQuot();
+lean_mark_persistent(l_Lean_Parser_checkOutsideQuot);
 l_Lean_Parser_hashOrelse___closed__1 = _init_l_Lean_Parser_hashOrelse___closed__1();
 lean_mark_persistent(l_Lean_Parser_hashOrelse___closed__1);
 l_Lean_Parser_hashOrelse = _init_l_Lean_Parser_hashOrelse();
diff --git a/stage0/stdlib/Lean/Parser/Extension.c b/stage0/stdlib/Lean/Parser/Extension.c
index a8a919f245..ce83acf6cb 100644
--- a/stage0/stdlib/Lean/Parser/Extension.c
+++ b/stage0/stdlib/Lean/Parser/Extension.c
@@ -8074,15 +8074,17 @@ return x_4;
 lean_object* l_Lean_Parser_mkParserContext(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6; 
 x_3 = l_Lean_Parser_getTokenTable(x_1);
 x_4 = lean_unsigned_to_nat(0u);
-x_5 = lean_alloc_ctor(0, 4, 0);
-lean_ctor_set(x_5, 0, x_2);
-lean_ctor_set(x_5, 1, x_4);
-lean_ctor_set(x_5, 2, x_1);
-lean_ctor_set(x_5, 3, x_3);
-return x_5;
+x_5 = 0;
+x_6 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_6, 0, x_2);
+lean_ctor_set(x_6, 1, x_4);
+lean_ctor_set(x_6, 2, x_1);
+lean_ctor_set(x_6, 3, x_3);
+lean_ctor_set_uint8(x_6, sizeof(void*)*4, x_5);
+return x_6;
 }
 }
 lean_object* l_Lean_Parser_mkParserState(lean_object* x_1) {
diff --git a/stage0/stdlib/Lean/Parser/Module.c b/stage0/stdlib/Lean/Parser/Module.c
index 16242ee05e..28accf2712 100644
--- a/stage0/stdlib/Lean/Parser/Module.c
+++ b/stage0/stdlib/Lean/Parser/Module.c
@@ -1995,45 +1995,48 @@ return x_1;
 }
 else
 {
-lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
 x_10 = lean_ctor_get(x_1, 0);
 x_11 = lean_ctor_get(x_1, 1);
 x_12 = lean_ctor_get(x_1, 2);
 x_13 = lean_ctor_get(x_1, 3);
+x_14 = lean_ctor_get_uint8(x_1, sizeof(void*)*4);
 lean_inc(x_13);
 lean_inc(x_12);
 lean_inc(x_11);
 lean_inc(x_10);
 lean_dec(x_1);
-x_14 = l_Lean_Parser_Module_header;
-x_15 = lean_ctor_get(x_14, 0);
-lean_inc(x_15);
-x_16 = l_Lean_Parser_addParserTokens(x_13, x_15);
-if (lean_obj_tag(x_16) == 0)
+x_15 = l_Lean_Parser_Module_header;
+x_16 = lean_ctor_get(x_15, 0);
+lean_inc(x_16);
+x_17 = l_Lean_Parser_addParserTokens(x_13, x_16);
+if (lean_obj_tag(x_17) == 0)
 {
-lean_object* x_17; lean_object* x_18; lean_object* x_19; 
-lean_dec(x_16);
-x_17 = l_Lean_Parser_Module_updateTokens___closed__1;
-x_18 = l_unreachable_x21___rarg(x_17);
-x_19 = lean_alloc_ctor(0, 4, 0);
-lean_ctor_set(x_19, 0, x_10);
-lean_ctor_set(x_19, 1, x_11);
-lean_ctor_set(x_19, 2, x_12);
-lean_ctor_set(x_19, 3, x_18);
-return x_19;
+lean_object* x_18; lean_object* x_19; lean_object* x_20; 
+lean_dec(x_17);
+x_18 = l_Lean_Parser_Module_updateTokens___closed__1;
+x_19 = l_unreachable_x21___rarg(x_18);
+x_20 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_20, 0, x_10);
+lean_ctor_set(x_20, 1, x_11);
+lean_ctor_set(x_20, 2, x_12);
+lean_ctor_set(x_20, 3, x_19);
+lean_ctor_set_uint8(x_20, sizeof(void*)*4, x_14);
+return x_20;
 }
 else
 {
-lean_object* x_20; lean_object* x_21; 
-x_20 = lean_ctor_get(x_16, 0);
-lean_inc(x_20);
-lean_dec(x_16);
-x_21 = lean_alloc_ctor(0, 4, 0);
-lean_ctor_set(x_21, 0, x_10);
-lean_ctor_set(x_21, 1, x_11);
-lean_ctor_set(x_21, 2, x_12);
-lean_ctor_set(x_21, 3, x_20);
-return x_21;
+lean_object* x_21; lean_object* x_22; 
+x_21 = lean_ctor_get(x_17, 0);
+lean_inc(x_21);
+lean_dec(x_17);
+x_22 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_22, 0, x_10);
+lean_ctor_set(x_22, 1, x_11);
+lean_ctor_set(x_22, 2, x_12);
+lean_ctor_set(x_22, 3, x_21);
+lean_ctor_set_uint8(x_22, sizeof(void*)*4, x_14);
+return x_22;
 }
 }
 }
diff --git a/stage0/stdlib/Lean/PrettyPrinter/Formatter.c b/stage0/stdlib/Lean/PrettyPrinter/Formatter.c
index 03ec7a5600..373cea4108 100644
--- a/stage0/stdlib/Lean/PrettyPrinter/Formatter.c
+++ b/stage0/stdlib/Lean/PrettyPrinter/Formatter.c
@@ -7359,7 +7359,7 @@ return x_5;
 lean_object* l_Lean_PrettyPrinter_Formatter_parseToken(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
 x_6 = lean_ctor_get(x_5, 0);
 lean_inc(x_6);
 x_7 = l_String_splitAux___main___closed__1;
@@ -7370,21 +7370,23 @@ lean_ctor_set(x_9, 0, x_1);
 lean_ctor_set(x_9, 1, x_7);
 lean_ctor_set(x_9, 2, x_8);
 x_10 = lean_unsigned_to_nat(0u);
-x_11 = lean_alloc_ctor(0, 4, 0);
-lean_ctor_set(x_11, 0, x_9);
-lean_ctor_set(x_11, 1, x_10);
-lean_ctor_set(x_11, 2, x_6);
-lean_ctor_set(x_11, 3, x_2);
-x_12 = l_Lean_Parser_mkParserState(x_1);
+x_11 = 0;
+x_12 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_12, 0, x_9);
+lean_ctor_set(x_12, 1, x_10);
+lean_ctor_set(x_12, 2, x_6);
+lean_ctor_set(x_12, 3, x_2);
+lean_ctor_set_uint8(x_12, sizeof(void*)*4, x_11);
+x_13 = l_Lean_Parser_mkParserState(x_1);
 lean_dec(x_1);
-x_13 = l_Lean_Parser_tokenFn(x_11, x_12);
-x_14 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_14, 0, x_13);
-lean_ctor_set(x_14, 1, x_3);
+x_14 = l_Lean_Parser_tokenFn(x_12, x_13);
 x_15 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_15, 0, x_14);
-lean_ctor_set(x_15, 1, x_5);
-return x_15;
+lean_ctor_set(x_15, 1, x_3);
+x_16 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_16, 0, x_15);
+lean_ctor_set(x_16, 1, x_5);
+return x_16;
 }
 }
 lean_object* l_Lean_PrettyPrinter_Formatter_parseToken___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
diff --git a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
index e7be270743..a115d8a941 100644
--- a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
+++ b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
@@ -77,6 +77,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer___lam
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___boxed(lean_object*);
 lean_object* lean_expr_update_mdata(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_MonadTraverser_goRight___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__4___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_identNoAntiquot_parenthesizer___boxed(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___closed__8;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__8;
@@ -165,8 +166,10 @@ lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesi
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2;
 lean_object* l_Lean_Meta_forallTelescope___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_range(lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_toggleInsideQuot_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___closed__21;
 lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___spec__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___boxed(lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkCombinatorParenthesizerAttribute___closed__1;
 lean_object* l_Lean_PrettyPrinter_parenthesizeCommand(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_setTailInfo(lean_object*, lean_object*);
@@ -407,6 +410,7 @@ lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesi
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
 lean_object* l_Lean_Syntax_MonadTraverser_getCur___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__1___boxed(lean_object*);
 extern lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___closed__2;
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__2;
 lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__13;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_symbol_parenthesizer___boxed(lean_object*);
@@ -435,6 +439,7 @@ lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___closed__7;
 lean_object* l_StateT_get___at_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___spec__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_ofExcept___at_Lean_PrettyPrinter_Parenthesizer_compileParenthesizerDescr___main___spec__1(lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_mkParenthesizerOfConstantUnsafe(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
@@ -569,6 +574,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoImmediateColon_parenthesi
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_identNoAntiquot_parenthesizer(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__1;
 lean_object* l_ReaderT_bind___at_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_lambdaTelescope___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_parenthesizeCommand___closed__1;
 lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__9;
@@ -586,6 +592,7 @@ lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lea
 lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___spec__24___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___spec__19(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer(lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___closed__1;
 lean_object* l_Lean_Syntax_MonadTraverser_goUp___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__4(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___lambda__34___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -600,6 +607,7 @@ lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesi
 lean_object* l_Std_PersistentArray_forM___at_IO_runMeta___spec__3(lean_object*, lean_object*);
 uint8_t l_Lean_Meta_TransparencyMode_lt(uint8_t, uint8_t);
 extern lean_object* l_PUnit_Inhabited;
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___lambda__33(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__3;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_nameLitNoAntiquot_parenthesizer(lean_object*);
@@ -700,6 +708,7 @@ extern lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__5;
 extern lean_object* l_Lean_defaultMaxRecDepth;
 lean_object* l_Lean_PrettyPrinter_categoryParenthesizerAttribute___closed__3;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_symbolNoWs_parenthesizer___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___boxed(lean_object*);
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___closed__15;
 lean_object* l_Lean_PrettyPrinter_categoryParenthesizerAttribute___closed__4;
@@ -13357,6 +13366,14 @@ lean_dec(x_1);
 return x_2;
 }
 }
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_toggleInsideQuot_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+lean_object* x_6; 
+x_6 = lean_apply_4(x_1, x_2, x_3, x_4, x_5);
+return x_6;
+}
+}
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@@ -13597,6 +13614,86 @@ lean_dec(x_1);
 return x_2;
 }
 }
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; 
+x_4 = lean_box(0);
+x_5 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_5, 0, x_4);
+lean_ctor_set(x_5, 1, x_1);
+x_6 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_6, 0, x_5);
+lean_ctor_set(x_6, 1, x_3);
+return x_6;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; 
+x_4 = lean_box(0);
+x_5 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_5, 0, x_4);
+lean_ctor_set(x_5, 1, x_1);
+x_6 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_6, 0, x_5);
+lean_ctor_set(x_6, 1, x_3);
+return x_6;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_pushNone_parenthesizer___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {