# HG changeset patch # User wenzelm # Date 1515935462 -3600 # Node ID 7d4a088dbc0e6a710666155d8e16a5c90eeceb9b # Parent 0b691782d6e5e6784e0f61a51ac09ffb7cb72729 clarified modules: uniform notion of formal comments; diff -r 0b691782d6e5 -r 7d4a088dbc0e src/Pure/General/comment.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/comment.ML Sun Jan 14 14:11:02 2018 +0100 @@ -0,0 +1,73 @@ +(* Title: Pure/General/comment.ML + Author: Makarius + +Formal comments. +*) + +signature COMMENT = +sig + datatype kind = Comment | Cancel + val scan_comment: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list + val scan_cancel: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list + val scan: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list + val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option +end; + +structure Comment: COMMENT = +struct + +(* kinds *) + +datatype kind = Comment | Cancel; + +val kinds = + [(Comment, {symbol = Symbol.comment, blanks = true}), + (Cancel, {symbol = Symbol.cancel, blanks = false})]; + +val get_kind = the o AList.lookup (op =) kinds; +val print_kind = quote o #symbol o get_kind; + +fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds; + + +(* scan *) + +local + +open Basic_Symbol_Pos; + +val err_prefix = "Error in formal comment: "; + +val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol); + +fun scan_symbol kind = + let val {blanks, symbol} = get_kind kind + in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end; + +fun scan_strict kind = + scan_symbol kind @@@ + Symbol_Pos.!!! (fn () => err_prefix ^ "cartouche expected after " ^ print_kind kind) + (Symbol_Pos.scan_cartouche err_prefix) >> pair kind; + +fun scan_permissive kind = + scan_symbol kind -- Scan.option (Symbol_Pos.scan_cartouche err_prefix) >> + (fn (ss, NONE) => (NONE, ss) | (_, SOME ss) => (SOME kind, ss)); + +in + +val scan_comment = scan_strict Comment; +val scan_cancel = scan_strict Cancel; +val scan = scan_comment || scan_cancel; + +val scan_body = + Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE || + scan_permissive Comment || scan_permissive Cancel; + +fun read_body syms = + if exists (is_symbol o Symbol_Pos.symbol) syms then + Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms + else NONE; + +end; + +end; diff -r 0b691782d6e5 -r 7d4a088dbc0e src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Sat Jan 13 21:41:36 2018 +0100 +++ b/src/Pure/General/symbol_pos.ML Sun Jan 14 14:11:02 2018 +0100 @@ -34,9 +34,6 @@ val scan_cartouche: string -> T list -> T list * T list val scan_cartouche_content: string -> T list -> T list * T list val recover_cartouche: T list -> T list * T list - val scan_blanks: T list -> T list * T list - val scan_cancel_cartouche: string -> T list -> T list * T list - val scan_comment_cartouche: string -> T list -> T list * T list val scan_comment: string -> T list -> T list * T list val scan_comment_body: string -> T list -> T list * T list val recover_comment: T list -> T list * T list @@ -219,19 +216,6 @@ val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth; -(* operator with cartouche argument *) - -val scan_blanks = Scan.many (Symbol.is_blank o symbol); - -fun scan_operator_cartouche blanks operator_symbol err_prefix = - (if blanks then $$$ operator_symbol @@@ scan_blanks else $$$ operator_symbol) @@@ - !!! (fn () => err_prefix ^ "cartouche expected after " ^ quote operator_symbol) - (scan_cartouche err_prefix); - -val scan_cancel_cartouche = scan_operator_cartouche false Symbol.cancel; -val scan_comment_cartouche = scan_operator_cartouche true Symbol.comment; - - (* ML-style comments *) local diff -r 0b691782d6e5 -r 7d4a088dbc0e src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Sat Jan 13 21:41:36 2018 +0100 +++ b/src/Pure/ML/ml_lex.ML Sun Jan 14 14:11:02 2018 +0100 @@ -9,7 +9,7 @@ val keywords: string list datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | - Space | Comment | Comment_Cartouche | Error of string | EOF + Space | Comment of Comment.kind option | Error of string | EOF eqtype token val stopper: token Scan.stopper val is_regular: token -> bool @@ -64,7 +64,7 @@ datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | - Space | Comment | Comment_Cartouche | Error of string | EOF; + Space | Comment of Comment.kind option | Error of string | EOF; datatype token = Token of Position.range * (token_kind * string); @@ -108,12 +108,10 @@ | is_regular _ = true; fun is_improper (Token (_, (Space, _))) = true - | is_improper (Token (_, (Comment, _))) = true - | is_improper (Token (_, (Comment_Cartouche, _))) = true + | is_improper (Token (_, (Comment _, _))) = true | is_improper _ = false; -fun is_comment (Token (_, (Comment, _))) = true - | is_comment (Token (_, (Comment_Cartouche, _))) = true +fun is_comment (Token (_, (Comment _, _))) = true | is_comment _ = false; fun warn tok = @@ -152,8 +150,7 @@ | Real => (Markup.ML_numeral, "") | Char => (Markup.ML_char, "") | String => (if SML then Markup.SML_string else Markup.ML_string, "") - | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "") - | Comment_Cartouche => (if SML then Markup.SML_comment else Markup.ML_comment, "") + | Comment _ => (if SML then Markup.SML_comment else Markup.ML_comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); @@ -178,7 +175,6 @@ open Basic_Symbol_Pos; val err_prefix = "SML lexical error: "; -val err_prefix' = "Isabelle/ML lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); @@ -299,8 +295,8 @@ (scan_char >> token Char || scan_string >> token String || scan_blanks1 >> token Space || - Symbol_Pos.scan_comment err_prefix >> token Comment || - Symbol_Pos.scan_comment_cartouche err_prefix' >> token Comment_Cartouche || + Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) || + Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) || Scan.max token_leq (Scan.literal lexicon >> token Keyword) (scan_word >> token Word || diff -r 0b691782d6e5 -r 7d4a088dbc0e src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Jan 13 21:41:36 2018 +0100 +++ b/src/Pure/ROOT.ML Sun Jan 14 14:11:02 2018 +0100 @@ -44,6 +44,7 @@ ML_file "General/position.ML"; ML_file "General/symbol_pos.ML"; ML_file "General/input.ML"; +ML_file "General/comment.ML"; ML_file "General/antiquote.ML"; ML_file "ML/ml_lex.ML"; ML_file "ML/ml_compiler1.ML"; diff -r 0b691782d6e5 -r 7d4a088dbc0e src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Sat Jan 13 21:41:36 2018 +0100 +++ b/src/Pure/Syntax/lexicon.ML Sun Jan 14 14:11:02 2018 +0100 @@ -22,7 +22,7 @@ val is_tid: string -> bool datatype token_kind = Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy | - StrSy | StringSy | Cartouche | Space | Cancel | Comment | Comment_Cartouche | EOF + StrSy | StringSy | Cartouche | Space | Comment of Comment.kind option | EOF datatype token = Token of token_kind * string * Position.range val kind_of_token: token -> token_kind val str_of_token: token -> string @@ -114,7 +114,7 @@ datatype token_kind = Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy | StrSy | - StringSy | Cartouche | Space | Cancel | Comment | Comment_Cartouche | EOF; + StringSy | Cartouche | Space | Comment of Comment.kind option | EOF; datatype token = Token of token_kind * string * Position.range; @@ -122,9 +122,7 @@ fun str_of_token (Token (_, s, _)) = s; fun pos_of_token (Token (_, _, (pos, _))) = pos; -val is_proper = - kind_of_token #> - (fn Space => false | Cancel => false | Comment => false | Comment_Cartouche => false | _ => true); +val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true); (* stopper *) @@ -169,7 +167,7 @@ | StrSy => Markup.inner_string | StringSy => Markup.inner_string | Cartouche => Markup.inner_cartouche - | Comment => Markup.inner_comment + | Comment NONE => Markup.inner_comment | _ => Markup.empty; fun report_of_token (Token (kind, s, (pos, _))) = @@ -268,9 +266,8 @@ val scan_token = Symbol_Pos.scan_cartouche err_prefix >> token Cartouche || - Symbol_Pos.scan_cancel_cartouche Symbol.cancel >> token Cancel || - Symbol_Pos.scan_comment err_prefix >> token Comment || - Symbol_Pos.scan_comment_cartouche err_prefix >> token Comment_Cartouche || + Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) || + Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) || Scan.max token_leq scan_lit scan_val || scan_string >> token StringSy || scan_str >> token StrSy || diff -r 0b691782d6e5 -r 7d4a088dbc0e src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Jan 13 21:41:36 2018 +0100 +++ b/src/Pure/Thy/thy_output.ML Sun Jan 14 14:11:02 2018 +0100 @@ -67,34 +67,7 @@ end; -(* output tokens with operators *) - -datatype operator = No_Operator | Cancel | Comment; - -local - -open Basic_Symbol_Pos; - -fun is_operator sym = sym = Symbol.cancel orelse sym = Symbol.comment; - -fun scan_operator blanks operator_symbol operator = - (if blanks then $$$ operator_symbol @@@ Symbol_Pos.scan_blanks else $$$ operator_symbol) -- - Scan.option (Symbol_Pos.scan_cartouche "Document token error: ") - >> (fn (syms, NONE) => (No_Operator, syms) | (_, SOME syms) => (operator, syms)); - -val scan_symbols_operator = - Scan.many1 (fn (s, _) => not (is_operator s) andalso Symbol.not_eof s) >> pair No_Operator || - scan_operator false Symbol.cancel Cancel || - scan_operator true Symbol.comment Comment; - -in - -fun read_symbols_operator syms = - if exists (is_operator o Symbol_Pos.symbol) syms then - Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_operator) syms - else NONE; - -end; +(* output tokens with formal comments *) local @@ -109,29 +82,29 @@ | Antiquote.Antiq {body, ...} => Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body)); -fun output_symbols_operator ctxt {antiq} (operator, syms) = - (case (operator, antiq) of - (No_Operator, false) => output_symbols syms - | (No_Operator, true) => +fun output_symbols_comment ctxt {antiq} (comment, syms) = + (case (comment, antiq) of + (NONE, false) => output_symbols syms + | (NONE, true) => Antiquote.parse (#1 (Symbol_Pos.range syms)) syms |> maps output_symbols_antiq - | (Cancel, _) => - output_symbols (Symbol_Pos.cartouche_content syms) - |> Latex.enclose_body "%\n\\isamarkupcancel{" "}" - | (Comment, _) => + | (SOME Comment.Comment, _) => let val body = Symbol_Pos.cartouche_content syms; val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body); in output_text ctxt {markdown = false} source |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}" - end); + end + | (SOME Comment.Cancel, _) => + output_symbols (Symbol_Pos.cartouche_content syms) + |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"); in fun output_body ctxt antiq bg en syms = - (case read_symbols_operator syms of - SOME res => maps (output_symbols_operator ctxt {antiq = antiq}) res + (case Comment.read_body syms of + SOME res => maps (output_symbols_comment ctxt {antiq = antiq}) res | NONE => output_symbols syms) |> Latex.enclose_body bg en and output_token ctxt tok = let @@ -153,19 +126,18 @@ end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); fun check_comments ctxt = - read_symbols_operator #> (Option.app o List.app) (fn (operator, syms) => + Comment.read_body #> (Option.app o List.app) (fn (comment, syms) => let val pos = #1 (Symbol_Pos.range syms); val markup = - (case operator of - No_Operator => NONE - | Cancel => SOME (Markup.language_text true) - | Comment => SOME (Markup.language_document true)); + comment |> Option.map + (fn Comment.Comment => Markup.language_document true + | Comment.Cancel => Markup.language_text true); val _ = markup |> Option.app (fn m => Context_Position.reports ctxt [(pos, m), (pos, Markup.cartouche)]); - val _ = output_symbols_operator ctxt {antiq = false} (operator, syms); - in if operator = Comment then check_comments ctxt syms else () end); + val _ = output_symbols_comment ctxt {antiq = false} (comment, syms); + in if comment = SOME Comment.Comment then check_comments ctxt syms else () end); fun check_token_comments ctxt tok = check_comments ctxt (Input.source_explode (Token.input_of tok)); diff -r 0b691782d6e5 -r 7d4a088dbc0e src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Sat Jan 13 21:41:36 2018 +0100 +++ b/src/Pure/Tools/rail.ML Sun Jan 14 14:11:02 2018 +0100 @@ -44,7 +44,7 @@ (* datatype token *) datatype kind = - Keyword | Ident | String | Space | Comment | Antiq of Antiquote.antiq | EOF; + Keyword | Ident | String | Space | Comment of Comment.kind | Antiq of Antiquote.antiq | EOF; datatype token = Token of Position.range * (kind * string); @@ -60,7 +60,7 @@ fun content_of (Token (_, (_, x))) = x; fun is_proper (Token (_, (Space, _))) = false - | is_proper (Token (_, (Comment, _))) = false + | is_proper (Token (_, (Comment _, _))) = false | is_proper _ = true; @@ -71,7 +71,7 @@ | Ident => "identifier" | String => "single-quoted string" | Space => "white space" - | Comment => "formal comment" + | Comment _ => "formal comment" | Antiq _ => "antiquotation" | EOF => "end-of-input"; @@ -118,7 +118,7 @@ val scan_token = scan_space >> token Space || - Symbol_Pos.scan_comment_cartouche err_prefix >> token Comment || + Comment.scan >> (fn (kind, ss) => token (Comment kind) ss)|| Antiquote.scan_antiq >> antiq_token || scan_keyword >> (token Keyword o single) || Lexicon.scan_id >> token Ident ||