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