changeset 55104 | 8284c0d5bf52 |
parent 55103 | 57d87ec3da4c |
child 55105 | 75815b3b38a1 |
--- a/src/Pure/Isar/token.ML Mon Jan 20 16:56:18 2014 +0100 +++ b/src/Pure/Isar/token.ML Mon Jan 20 19:47:31 2014 +0100 @@ -336,7 +336,8 @@ (* scan cartouche *) val scan_cartouche = - Symbol_Pos.scan_pos -- (Symbol_Pos.scan_cartouche_body !!! -- Symbol_Pos.scan_pos); + Symbol_Pos.scan_pos -- + ((Symbol_Pos.scan_cartouche !!! >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos); (* scan space *)