adbrucker
/
isabelle-hacks
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Made top-level user interface more consistent.

This commit is contained in:
Achim D. Brucker 2018-06-21 21:34:57 +01:00
parent 92ea551113
commit 66307c1c2b
1 changed files with 20 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
Hiding_Type_Variables.thy
View File

@ -49,8 +49,8 @@ text\<open>This theory implements a mechanism for declaring default type
section\<open>Theory Managed Data Structure\<close> section\<open>Theory Managed Data Structure\<close>
ML\<open> ML\<open>
signature HIDE_TVAR = sig signature HIDE_TVAR = sig
datatype print_mode = always | default_only | noprint datatype print_mode = print_all | print | noprint
datatype parse_mode = active | noparse datatype parse_mode = parse | noparse
type hide_varT = { type hide_varT = {
name: string, name: string,
tvars: typ list, tvars: typ list,
@ -70,8 +70,8 @@ signature HIDE_TVAR = sig
end end
structure Hide_Tvar : HIDE_TVAR = struct structure Hide_Tvar : HIDE_TVAR = struct
datatype print_mode = always | default_only | noprint datatype print_mode = print_all | print | noprint
datatype parse_mode = active | noparse datatype parse_mode = parse | noparse
type hide_varT = { type hide_varT = {
name: string, name: string,
tvars: typ list, tvars: typ list,
@ -92,14 +92,14 @@ structure Hide_Tvar : HIDE_TVAR = struct
); );
fun parse_print_mode "always" = always fun parse_print_mode "print_all" = print_all
| parse_print_mode "default_only" = default_only | parse_print_mode "print" = print
| parse_print_mode "noprint" = noprint | parse_print_mode "noprint" = noprint
| parse_print_mode s = error("Print mode not supported: "^s) | parse_print_mode s = error("Print mode not supported: "^s)
fun parse_parse_mode "active" = active fun parse_parse_mode "parse" = parse
| parse_parse_mode "noparse" = noparse | parse_parse_mode "noparse" = noparse
| parse_parse_mode s = error("Parse mode not supported: "^s) | parse_parse_mode s = error("Parse mode not supported: "^s)
fun update_mode typ_str print_mode parse_mode thy = fun update_mode typ_str print_mode parse_mode thy =
let let
@ -249,8 +249,8 @@ structure Hide_Tvar : HIDE_TVAR = struct
| SOME (s,_) => local_name_of s | SOME (s,_) => local_name_of s
in in
case (#print_mode e) of case (#print_mode e) of
always => hide_type tname print_all => hide_type tname
| default_only => hide_type tname (* TODO *) | print => hide_type tname (* TODO *)
| noprint => raise Match | noprint => raise Match
end end
end end
@ -293,10 +293,10 @@ structure Hide_Tvar : HIDE_TVAR = struct
val print_m = case print_mode of val print_m = case print_mode of
SOME m => m SOME m => m
| NONE => always | NONE => print_all
val parse_m = case parse_mode of val parse_m = case parse_mode of
SOME m => m SOME m => m
| NONE => active | NONE => parse
val entry = { val entry = {
name = name, name = name,
tvars = tvars, tvars = tvars,
@ -360,7 +360,7 @@ ML\<open>
|-- (Parse.name --| Parse.$$$ "," |-- (Parse.name --| Parse.$$$ ","
-- Parse.name --| -- Parse.name --|
Parse.$$$ ")")) Parse.$$$ ")"))
val typ_modeP = Parse.typ -- (Scan.optional modeP ("always","active")) val typ_modeP = Parse.typ -- (Scan.optional modeP ("print_all","parse"))
val _ = Outer_Syntax.command @{command_keyword "register_default_tvars"} val _ = Outer_Syntax.command @{command_keyword "register_default_tvars"}
"Register default variables (and hiding mechanims) for a type." "Register default variables (and hiding mechanims) for a type."
@ -396,8 +396,8 @@ assert[string_of_thm_equal,
thm_def="g_def", thm_def="g_def",
str="g (a::('a + 'b, 'a \<times> 'b) foobar) (b::('a + 'b, 'a \<times> 'b) foobar) = a"] str="g (a::('a + 'b, 'a \<times> 'b) foobar) (b::('a + 'b, 'a \<times> 'b) foobar) = a"]
register_default_tvars "('alpha, 'beta) foobar" (always,active) register_default_tvars "('alpha, 'beta) foobar" (print_all,parse)
register_default_tvars "('alpha, 'beta, 'gamma, 'delta) baz" (always,active) register_default_tvars "('alpha, 'beta, 'gamma, 'delta) baz" (print_all,parse)
update_default_tvars_mode "_ foobar" (noprint,noparse) update_default_tvars_mode "_ foobar" (noprint,noparse)
assert[string_of_thm_equal, assert[string_of_thm_equal,
@ -407,7 +407,7 @@ assert[string_of_thm_equal,
thm_def="g_def", thm_def="g_def",
str="g (a::('a + 'b, 'a \<times> 'b) foobar) (b::('a + 'b, 'a \<times> 'b) foobar) = a"] str="g (a::('a + 'b, 'a \<times> 'b) foobar) (b::('a + 'b, 'a \<times> 'b) foobar) = a"]
update_default_tvars_mode "_ foobar" (always,noparse) update_default_tvars_mode "_ foobar" (print_all,noparse)
assert[string_of_thm_equal, assert[string_of_thm_equal,
thm_def="f_def", str="f (a::(_) foobar) (b::(_) foobar) = a"] thm_def="f_def", str="f (a::(_) foobar) (b::(_) foobar) = a"]
@ -415,7 +415,7 @@ assert[string_of_thm_equal,
thm_def="g_def", str="g (a::(_) baz) (b::(_) baz) = a"] thm_def="g_def", str="g (a::(_) baz) (b::(_) baz) = a"]
subsection\<open>Parse Translation\<close> subsection\<open>Parse Translation\<close>
update_default_tvars_mode "_ foobar" (noprint,active) update_default_tvars_mode "_ foobar" (print_all,parse)
declare [[show_types]] declare [[show_types]]
definition A :: "'alpha \<Rightarrow> (_) foobar" definition A :: "'alpha \<Rightarrow> (_) foobar"