inner syntax comments may be written as "\<comment> \<open>text\<close>";
authorwenzelm
Sat Jan 06 16:56:07 2018 +0100 (17 months ago)
changeset 673525f7f339f3d7e
parent 67346 1f1d85393d70
child 67353 95f5f4bec7af
inner syntax comments may be written as "\<comment> \<open>text\<close>";
NEWS
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Pure/Syntax/lexicon.ML
     1.1 --- a/NEWS	Sat Jan 06 15:08:42 2018 +0100
     1.2 +++ b/NEWS	Sat Jan 06 16:56:07 2018 +0100
     1.3 @@ -9,6 +9,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Inner syntax comments may be written as "\<comment> \<open>text\<close>", similar to
     1.8 +marginal comments in outer syntax.
     1.9 +
    1.10  * The old 'def' command has been discontinued (legacy since
    1.11  Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
    1.12  object-logic equality or equivalence.
     2.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 06 15:08:42 2018 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 06 16:56:07 2018 +0100
     2.3 @@ -565,6 +565,7 @@
     2.4      @{syntax_def (inner) str_token} & = & \<^verbatim>\<open>''\<close> \<open>\<dots>\<close> \<^verbatim>\<open>''\<close> \\
     2.5      @{syntax_def (inner) string_token} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
     2.6      @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
     2.7 +    @{syntax_def (inner) comment_cartouche} & = & @{verbatim "\<comment> \<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
     2.8    \end{supertabular}
     2.9    \end{center}
    2.10  
    2.11 @@ -578,6 +579,11 @@
    2.12    The derived categories @{syntax_def (inner) num_const}, and @{syntax_def
    2.13    (inner) float_const}, provide robust access to the respective tokens: the
    2.14    syntax tree holds a syntactic constant instead of a free variable.
    2.15 +
    2.16 +  A @{syntax (inner) comment_cartouche} resembles the outer syntax notation
    2.17 +  for marginal @{syntax_ref comment} (\secref{sec:comments}), but is
    2.18 +  syntactically more restrictive: only the symbol-form with \<^verbatim>\<open>\<comment>\<close> and text
    2.19 +  cartouche is supported.
    2.20  \<close>
    2.21  
    2.22  
     3.1 --- a/src/Pure/Syntax/lexicon.ML	Sat Jan 06 15:08:42 2018 +0100
     3.2 +++ b/src/Pure/Syntax/lexicon.ML	Sat Jan 06 16:56:07 2018 +0100
     3.3 @@ -21,8 +21,8 @@
     3.4    val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
     3.5    val is_tid: string -> bool
     3.6    datatype token_kind =
     3.7 -    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy |
     3.8 -    FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF
     3.9 +    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy |
    3.10 +    StrSy | StringSy | Cartouche | Space | Comment | Comment_Cartouche| EOF
    3.11    datatype token = Token of token_kind * string * Position.range
    3.12    val str_of_token: token -> string
    3.13    val pos_of_token: token -> Position.T
    3.14 @@ -112,8 +112,8 @@
    3.15  (** datatype token **)
    3.16  
    3.17  datatype token_kind =
    3.18 -  Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy |
    3.19 -  FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF;
    3.20 +  Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy | StrSy |
    3.21 +  StringSy | Cartouche | Space | Comment | Comment_Cartouche | EOF;
    3.22  
    3.23  datatype token = Token of token_kind * string * Position.range;
    3.24  
    3.25 @@ -122,6 +122,7 @@
    3.26  
    3.27  fun is_proper (Token (Space, _, _)) = false
    3.28    | is_proper (Token (Comment, _, _)) = false
    3.29 +  | is_proper (Token (Comment_Cartouche, _, _)) = false
    3.30    | is_proper _ = true;
    3.31  
    3.32  
    3.33 @@ -170,6 +171,7 @@
    3.34    | StringSy => Markup.inner_string
    3.35    | Cartouche => Markup.inner_cartouche
    3.36    | Comment => Markup.inner_comment
    3.37 +  | Comment_Cartouche => Markup.inner_comment
    3.38    | _ => Markup.empty;
    3.39  
    3.40  fun report_of_token (Token (kind, s, (pos, _))) =
    3.41 @@ -244,6 +246,12 @@
    3.42  val explode_str = explode_literal scan_str_body;
    3.43  
    3.44  
    3.45 +(* comment cartouche *)
    3.46 +
    3.47 +val scan_comment_cartouche =
    3.48 +  $$$ "\<comment>" @@@ Scan.many (Symbol.is_blank o Symbol_Pos.symbol) @@@
    3.49 +    !!! "cartouche expected after \"\<comment>\"" (Symbol_Pos.scan_cartouche err_prefix);
    3.50 +
    3.51  
    3.52  (** tokenize **)
    3.53  
    3.54 @@ -270,6 +278,7 @@
    3.55      val scan_token =
    3.56        Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
    3.57        Symbol_Pos.scan_comment err_prefix >> token Comment ||
    3.58 +      scan_comment_cartouche >> token Comment_Cartouche ||
    3.59        Scan.max token_leq scan_lit scan_val ||
    3.60        scan_string >> token StringSy ||
    3.61        scan_str >> token StrSy ||