equal
deleted
inserted
replaced
46 |
46 |
47 File.write_backup(output_path, """{ |
47 File.write_backup(output_path, """{ |
48 "name": "Isabelle", |
48 "name": "Isabelle", |
49 "scopeName": "source.isabelle", |
49 "scopeName": "source.isabelle", |
50 "fileTypes": ["thy"], |
50 "fileTypes": ["thy"], |
51 "uuid": """ + JSON.Format(UUID.random().toString) + """, |
51 "uuid": """ + JSON.Format(UUID.random_string()) + """, |
52 "repository": { |
52 "repository": { |
53 "comment": { |
53 "comment": { |
54 "patterns": [ |
54 "patterns": [ |
55 { |
55 { |
56 "name": "comment.block.isabelle", |
56 "name": "comment.block.isabelle", |