more thorough check_command, including completion;
authorwenzelm
Tue Nov 10 20:49:48 2015 +0100 (2015-11-10)
changeset 6161827af754f50ca
parent 61617 cd7549cd5fe7
child 61619 f22054b192b0
more thorough check_command, including completion;
src/Doc/antiquote_setup.ML
src/Pure/Isar/keyword.ML
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Nov 10 20:10:17 2015 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Nov 10 20:49:48 2015 +0100
     1.3 @@ -150,20 +150,7 @@
     1.4  fun is_keyword ctxt (name, _) =
     1.5    Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name;
     1.6  
     1.7 -fun check_command ctxt (name, pos) =
     1.8 -  let
     1.9 -    val thy = Proof_Context.theory_of ctxt;
    1.10 -    val keywords = Thy_Header.get_keywords thy;
    1.11 -  in
    1.12 -    Keyword.is_command keywords name andalso
    1.13 -      let
    1.14 -        val markup =
    1.15 -          Token.explode keywords Position.none name
    1.16 -          |> maps (Outer_Syntax.command_reports thy)
    1.17 -          |> map (snd o fst);
    1.18 -        val _ = Context_Position.reports ctxt (map (pair pos) markup);
    1.19 -      in true end
    1.20 -  end;
    1.21 +fun check_command ctxt (name, pos) = (Outer_Syntax.check_command ctxt (name, pos); true);
    1.22  
    1.23  fun check_system_option ctxt (name, pos) =
    1.24    (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
     2.1 --- a/src/Pure/Isar/keyword.ML	Tue Nov 10 20:10:17 2015 +0100
     2.2 +++ b/src/Pure/Isar/keyword.ML	Tue Nov 10 20:49:48 2015 +0100
     2.3 @@ -43,6 +43,7 @@
     2.4    val is_keyword: keywords -> string -> bool
     2.5    val is_command: keywords -> string -> bool
     2.6    val is_literal: keywords -> string -> bool
     2.7 +  val dest_commands: keywords -> string list
     2.8    val command_markup: keywords -> string -> Markup.T option
     2.9    val command_kind: keywords -> string -> string option
    2.10    val command_files: keywords -> string -> Path.T -> Path.T list
    2.11 @@ -187,6 +188,8 @@
    2.12  fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
    2.13  fun is_literal keywords = is_keyword keywords orf is_command keywords;
    2.14  
    2.15 +fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands;
    2.16 +
    2.17  
    2.18  (* command keywords *)
    2.19  
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Nov 10 20:10:17 2015 +0100
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Nov 10 20:49:48 2015 +0100
     3.3 @@ -25,6 +25,7 @@
     3.4    val parse_spans: Token.T list -> Command_Span.span list
     3.5    val side_comments: Token.T list -> Token.T list
     3.6    val command_reports: theory -> Token.T -> Position.report_text list
     3.7 +  val check_command: Proof.context -> string * Position.T -> string
     3.8  end;
     3.9  
    3.10  structure Outer_Syntax: OUTER_SYNTAX =
    3.11 @@ -268,7 +269,7 @@
    3.12  val side_comments = filter Token.is_proper #> cmts;
    3.13  
    3.14  
    3.15 -(* read commands *)
    3.16 +(* check commands *)
    3.17  
    3.18  fun command_reports thy tok =
    3.19    if Token.is_command tok then
    3.20 @@ -279,4 +280,30 @@
    3.21      end
    3.22    else [];
    3.23  
    3.24 +fun check_command ctxt (name, pos) =
    3.25 +  let
    3.26 +    val thy = Proof_Context.theory_of ctxt;
    3.27 +    val keywords = Thy_Header.get_keywords thy;
    3.28 +  in
    3.29 +    if Keyword.is_command keywords name then
    3.30 +      let
    3.31 +        val markup =
    3.32 +          Token.explode keywords Position.none name
    3.33 +          |> maps (command_reports thy)
    3.34 +          |> map (#2 o #1);
    3.35 +        val _ = Context_Position.reports ctxt (map (pair pos) markup);
    3.36 +      in name end
    3.37 +    else
    3.38 +      let
    3.39 +        val completion =
    3.40 +          Completion.make (name, pos)
    3.41 +            (fn completed =>
    3.42 +              Keyword.dest_commands keywords
    3.43 +              |> filter completed
    3.44 +              |> sort_strings
    3.45 +              |> map (fn a => (a, (Markup.commandN, a))));
    3.46 +        val report = Markup.markup_report (Completion.reported_text completion);
    3.47 +      in error ("Bad command " ^ quote name ^ Position.here pos ^ report) end
    3.48 +  end;
    3.49 +
    3.50  end;