[isabelle] Use/problem about {*...*} braces; single quote in path causes problem



Hi,

I'm here because I don't want to be, and prefer no feedback. The past is the future. C and Perl are never going away.

This email is about the use of {*...*} braces, and that a single quote in my theory path possibly causes problems with `File.platform_path (Resources.master_directory (Toplevel.theory_of state))`. None of this is a show-stopper.

A while back M.Wenzel asked why old-style braces {*...*} are needed any longer.

OLD-STYLE DELIMITER USE:

I respond to that with two comments:

1) I was doing some tokening on `\<open>` and `\<close>` in a `ML` statement. I found that I don't have to use them in matched pairs in a `ML{*...*}`, but I do in a `ML\<open>...\<close>`. I include some source to demonstrate the problem below.

2) I attach a screen shot which shows that `{*...*}` is potentially useful in place of `\<open>...\<close>` or `"..."`. If it's there I might use it to keep from nesting cartouche delimiters, to make things easier to read.

SINGLE QUOTES IN MY PATH REDUCE IT TO DOT:

That's demonstrated in the included source. I put it first before the cartouche problem. It's not a problem. I just don't use a path with a single quote in it.

The image is attached to show my use of {*...*}.

Regards,
GB

THE SOURCE:

theory Scratch
imports Complex_Main
keywords "Foo" :: diag
begin
ML{*Outer_Syntax.command @{command_keyword "Foo"}
"Test to show single quotes in the path cause problems"
(Parse.text >> (fn _ => Toplevel.keep (fn state =>
let
  val thyPath = File.platform_path
  (Resources.master_directory (Toplevel.theory_of state))
in
  writeln (File.shell_quote thyPath)
end)))*}

Foo{**} (*If I have this in path "E:\_t'est", it prints '.'.*)

(*WORKS*)
ML{* val lcartouche = "\<open>" *}

(*WORKS*)
ML\<open>
val lcartouche = "\<open>";
val rcartouche = "\<close>"
\<close>

(*CAUSES ERROR: Malformed command syntax*)
ML\<open>
val lcartouche = "\<open>"
\<close>

end


Attachment: 150722_use_for_brace_star_delim.png
Description: PNG image



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.