clarified signature;
authorwenzelm
Sat Dec 16 12:16:40 2017 +0100 (17 months ago)
changeset 6720816519cd83ed4
parent 67207 ad538f6c5d2f
child 67209 fca5f2988091
clarified signature;
src/Pure/General/completion.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/System/options.ML
     1.1 --- a/src/Pure/General/completion.ML	Thu Dec 14 18:42:39 2017 +0100
     1.2 +++ b/src/Pure/General/completion.ML	Sat Dec 16 12:16:40 2017 +0100
     1.3 @@ -13,6 +13,9 @@
     1.4    val encode: T -> XML.body
     1.5    val reported_text: T -> string
     1.6    val suppress_abbrevs: string -> Markup.T list
     1.7 +  val check_option: Options.T -> Proof.context -> string * Position.T -> string
     1.8 +  val check_option_value:
     1.9 +    Proof.context -> string * Position.T -> string * Position.T -> Options.T -> string * Options.T
    1.10  end;
    1.11  
    1.12  structure Completion: COMPLETION =
    1.13 @@ -64,4 +67,30 @@
    1.14    then [Markup.no_completion]
    1.15    else [];
    1.16  
    1.17 +
    1.18 +(* system options *)
    1.19 +
    1.20 +fun check_option options ctxt (name, pos) =
    1.21 +  let
    1.22 +    val markup =
    1.23 +      Options.markup options (name, pos) handle ERROR msg =>
    1.24 +        let
    1.25 +          val completion =
    1.26 +            make (name, pos) (fn completed =>
    1.27 +                Options.names options
    1.28 +                |> filter completed
    1.29 +                |> map (fn a => (a, ("system_option", a))));
    1.30 +          val report = Markup.markup_report (reported_text completion);
    1.31 +        in error (msg ^ report) end;
    1.32 +    val _ = Context_Position.report ctxt pos markup;
    1.33 +  in name end;
    1.34 +
    1.35 +fun check_option_value ctxt (name, pos) (value, pos') options =
    1.36 +  let
    1.37 +    val _ = check_option options ctxt (name, pos);
    1.38 +    val options' =
    1.39 +      Options.update name value options
    1.40 +        handle ERROR msg => error (msg ^ Position.here pos');
    1.41 +  in (name, options') end;
    1.42 +
    1.43  end;
     2.1 --- a/src/Pure/ML/ml_antiquotations.ML	Thu Dec 14 18:42:39 2017 +0100
     2.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Sat Dec 16 12:16:40 2017 +0100
     2.3 @@ -42,19 +42,7 @@
     2.4  val _ = Theory.setup
     2.5   (ML_Antiquotation.value \<^binding>\<open>system_option\<close>
     2.6      (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
     2.7 -      let
     2.8 -        val markup =
     2.9 -          Options.default_markup (name, pos) handle ERROR msg =>
    2.10 -            let
    2.11 -              val completion =
    2.12 -                Completion.make (name, pos) (fn completed =>
    2.13 -                    Options.names (Options.default ())
    2.14 -                    |> filter completed
    2.15 -                    |> map (fn a => (a, ("system_option", a))));
    2.16 -              val report = Markup.markup_report (Completion.reported_text completion);
    2.17 -            in error (msg ^ report) end;
    2.18 -        val _ = Context_Position.report ctxt pos markup;
    2.19 -      in ML_Syntax.print_string name end)) #>
    2.20 +      (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #>
    2.21  
    2.22    ML_Antiquotation.value \<^binding>\<open>theory\<close>
    2.23      (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
     3.1 --- a/src/Pure/System/options.ML	Thu Dec 14 18:42:39 2017 +0100
     3.2 +++ b/src/Pure/System/options.ML	Sat Dec 16 12:16:40 2017 +0100
     3.3 @@ -29,7 +29,6 @@
     3.4    val update: string -> string -> T -> T
     3.5    val decode: XML.body -> T
     3.6    val default: unit -> T
     3.7 -  val default_markup: string * Position.T -> Markup.T
     3.8    val default_typ: string -> string
     3.9    val default_bool: string -> bool
    3.10    val default_int: string -> int
    3.11 @@ -189,7 +188,6 @@
    3.12      SOME options => options
    3.13    | NONE => err_no_default ());
    3.14  
    3.15 -fun default_markup arg = markup (default ()) arg;
    3.16  fun default_typ name = typ (default ()) name;
    3.17  fun default_bool name = bool (default ()) name;
    3.18  fun default_int name = int (default ()) name;